Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Nonlin LA preds #790

Open
wants to merge 20 commits into
base: master
Choose a base branch
from
Open

Nonlin LA preds #790

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
06306c8
NonlinWork: initial commit
BritikovKI Oct 29, 2024
59c9152
NonlinWork: additional fixes concerning division and nonlin
BritikovKI Oct 29, 2024
9afd418
NonlinWork: fix of tests and code rework
BritikovKI Oct 30, 2024
9555791
NonlinWork: PR cleanup
BritikovKI Oct 31, 2024
b64f03b
NonlinWork: added PR-connected regression tests
BritikovKI Nov 3, 2024
b617b20
NonlinWork: added support for mod
BritikovKI Nov 4, 2024
2f49d40
NonlinWork: moved and updated the Nonlin checks, tests rework, except…
BritikovKI Nov 5, 2024
9bc9c8a
NonlinWork: catching exceptions, few fixes
BritikovKI Nov 6, 2024
046a7b9
NonlinWork: update to atomic Nonlin checks, propper checks in the LAS…
BritikovKI Nov 7, 2024
fab2f08
NonlinWork: fix of the print in MainSolver
BritikovKI Nov 8, 2024
a236b36
NonlinWork: changed splitTerm
BritikovKI Nov 13, 2024
2eedd00
NonlinWork: changes in multiplication handling
BritikovKI Nov 14, 2024
8ff3d59
NonlinWork: single symbol for multiplication
BritikovKI Nov 18, 2024
d8ecbb6
NonlinWork: duplicate symbol creation
BritikovKI Nov 19, 2024
d8953ac
NonlinWork: SubSymbol notion
BritikovKI Nov 19, 2024
3829c5c
NonlinWork: added sym_Int_TIMES_LIN
BritikovKI Nov 20, 2024
68ac42d
NonlinWork: added new functions, rework of the accessible parts
BritikovKI Nov 25, 2024
1668eff
NonlinWork: Fixes according to comments
BritikovKI Nov 28, 2024
adaea42
NonlinWork: Nonlin Real division is no longer supported
BritikovKI Nov 29, 2024
cdb3164
NonlinWork: small fixes and optimisations
BritikovKI Dec 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 4 additions & 7 deletions src/logics/ArithLogic.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,10 +114,8 @@ ArithLogic::ArithLogic(Logic_t type)
sym_Real_MINUS(declareFun_NoScoping_LeftAssoc(tk_real_minus, sort_REAL, {sort_REAL, sort_REAL})),
sym_Real_PLUS(declareFun_Commutative_NoScoping_LeftAssoc(tk_real_plus, sort_REAL, {sort_REAL, sort_REAL})),
sym_Real_TIMES(declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})),
sym_Real_TIMES_LIN(
declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times, sort_REAL, {sort_REAL, sort_REAL}, true)),
sym_Real_TIMES_NONLIN(
declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times, sort_REAL, {sort_REAL, sort_REAL}, true)),
sym_Real_TIMES_LIN(declareFun_Multiplication_Duplicate(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})),
sym_Real_TIMES_NONLIN(declareFun_Multiplication_Duplicate(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})),
BritikovKI marked this conversation as resolved.
Show resolved Hide resolved
sym_Real_DIV(declareFun_NoScoping_LeftAssoc(tk_real_div, sort_REAL, {sort_REAL, sort_REAL})),
sym_Real_EQ(sortToEquality[sort_REAL]),
sym_Real_LEQ(declareFun_NoScoping_Chainable(tk_real_leq, sort_BOOL, {sort_REAL, sort_REAL})),
Expand All @@ -138,9 +136,8 @@ ArithLogic::ArithLogic(Logic_t type)
sym_Int_MINUS(declareFun_NoScoping_LeftAssoc(tk_int_minus, sort_INT, {sort_INT, sort_INT})),
sym_Int_PLUS(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_plus, sort_INT, {sort_INT, sort_INT})),
sym_Int_TIMES(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times, sort_INT, {sort_INT, sort_INT})),
sym_Int_TIMES_LIN(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times, sort_INT, {sort_INT, sort_INT}, true)),
sym_Int_TIMES_NONLIN(
declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times, sort_INT, {sort_INT, sort_INT}, true)),
sym_Int_TIMES_LIN(declareFun_Multiplication_Duplicate(tk_int_times, sort_INT, {sort_INT, sort_INT})),
sym_Int_TIMES_NONLIN(declareFun_Multiplication_Duplicate(tk_int_times, sort_INT, {sort_INT, sort_INT})),
sym_Int_DIV(declareFun_NoScoping_LeftAssoc(tk_int_div, sort_INT, {sort_INT, sort_INT})),
sym_Int_MOD(declareFun_NoScoping(tk_int_mod, sort_INT, {sort_INT, sort_INT})),
sym_Int_EQ(sortToEquality[sort_INT]),
Expand Down
4 changes: 2 additions & 2 deletions src/logics/Logic.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -728,11 +728,11 @@ PTRef Logic::mkSelect(vec<PTRef> && args) {
}

SymRef Logic::declareFun(std::string const & fname, SRef rsort, vec<SRef> const & args,
SymbolConfig const & symbolConfig, bool subSymb) {
SymbolConfig const & symbolConfig) {
assert(rsort != SRef_Undef);
assert(std::find(args.begin(), args.end(), SRef_Undef) == args.end());

SymRef sr = sym_store.newSymb(fname.c_str(), rsort, args, symbolConfig, subSymb);
SymRef sr = sym_store.newSymb(fname.c_str(), rsort, args, symbolConfig);
return sr;
}

Expand Down
12 changes: 7 additions & 5 deletions src/logics/Logic.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -164,8 +164,7 @@ class Logic {
virtual PTRef mkConst(char const *);
virtual PTRef mkConst(SRef, char const *);

SymRef declareFun(std::string const & fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symbolConfig,
bool duplicate = false);
SymRef declareFun(std::string const & fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symbolConfig);
SymRef declareFun(std::string const & fname, SRef rsort, vec<SRef> const & args) {
return declareFun(fname, rsort, args, SymConf::Default);
}
Expand All @@ -184,9 +183,12 @@ class Logic {
SymRef declareFun_NoScoping_Pairwise(std::string const & s, SRef rsort, vec<SRef> const & args) {
return declareFun(s, rsort, args, SymConf::NoScopingPairwise);
}
SymRef declareFun_Commutative_NoScoping_LeftAssoc(std::string const & s, SRef rsort, vec<SRef> const & args,
bool subSymb = false) {
return declareFun(s, rsort, args, SymConf::CommutativeNoScopingLeftAssoc, subSymb);
SymRef declareFun_Commutative_NoScoping_LeftAssoc(std::string const & s, SRef rsort, vec<SRef> const & args) {
return declareFun(s, rsort, args, SymConf::CommutativeNoScopingLeftAssoc);
}
SymRef declareFun_Multiplication_Duplicate(std::string const & s, SRef rsort, vec<SRef> const & args) {
BritikovKI marked this conversation as resolved.
Show resolved Hide resolved
SymRef sr = sym_store.newUnparsableSymb(s.c_str(), rsort, args, SymConf::CommutativeNoScopingLeftAssoc);
return sr;
}
SymRef declareFun_Commutative_NoScoping_Chainable(std::string const & s, SRef rsort, vec<SRef> const & args) {
return declareFun(s, rsort, args, SymConf::CommutativeNoScopingChainable);
Expand Down
4 changes: 4 additions & 0 deletions src/symbols/SymStore.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,11 +40,15 @@ class SymStore {
SymStore(SymStore &&) = default;
SymStore & operator=(SymStore &&) = default;
// Constructs a new symbol.

SymRef newSymb(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig,
BritikovKI marked this conversation as resolved.
Show resolved Hide resolved
bool subSymb = false);
SymRef newSymb(char const * fname, SRef rsort, vec<SRef> const & args) {
return newSymb(fname, rsort, args, SymConf::Default);
}
SymRef newUnparsableSymb(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig) {
BritikovKI marked this conversation as resolved.
Show resolved Hide resolved
return newSymb(fname, rsort, args, symConfig, true);
}
bool contains(char const * fname) const { return symbolTable.has(fname); }
vec<SymRef> const & nameToRef(char const * s) const { return symbolTable[s]; }
vec<SymRef> & nameToRef(char const * s) { return symbolTable[s]; }
Expand Down