| Age | Commit message (Collapse) | Author |
|---|
|
hasTrichotomyProof().
|
|
existing bound.
|
|
|
|
|
|
|
|
|
|
not negBack is already in conflict. This is needed as it can be called multiple times on the same constraint.
|
|
|
|
|
|
This commit adds tracking of Farkas coefficients to proof enabled builds in the theory of linear
real arithmetic when proofs are enabled. There could be some performance changes due to subtly
different search paths being taken.
Additional bug fixes:
- Polynomial::exactDivide did not satisfy preconditions to the Monomial constructor.
To prevent future problems, Monomials should now be made via one of the mkMonomial functions.
- Fixes a bug in SumOfInfeasibilitiesSPD::greedyConflictSubsets().
There was a way to use a row twice in the construction of the conflicts.
This was violating an assumption in the Tableau when constructing the intermediate rows.
Constraints:
- To enable proofs, all conflicts and propagations are designed to go through the Constraint system
before they are converted to externally understandable conflicts and propagations in the form
of Node.
- Constraints must now be given a reason for marking them as true that corresponds to a proof.
- Constraints should now be marked as being true by one of the impliedbyX functions.
- Each impliedByX function has an ArithProofType associated with it.
- Each call to an impliedByX function stores a context dependent ConstraintRule object
to track the proof.
- After marking the node as true the caller should either try to propagate the constraint or raise
a conflict.
- There are no more special cases for marking a node as being true when its negation has a proof
vs. when the negation does not have a proof. One must now explicitly pass in a inConflict flag
to the impliedByX (and similar functions).
For example,this is now longer both:
void setAssertedToTheTheory(TNode witness);
void setAssertedToTheTheoryWithNegationTrue(TNode witness);
There is just:
void setAssertedToTheTheory(TNode witness, bool inConflict);
|
|
|
|
trigger terms. I've disabled constants as triggers for all equality engines
except for the shared terms engine where it is needed.
|
|
|
|
|
|
* Add TheorySets::getEqualityStatus(TNode, TNode)
* Add TheorySets::getModelValue(TNode)
|
|
|
|
|
|
|
|
|
|
and arith.
|
|
|
|
|
|
|
|
|
|
compilation troubles with libc++.
|
|
|
|
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
|
|
types get sent to the theory of the type.
Adding a new test case for bug 569.
Fixes to the normal form of arithmetic so that real terms are before integer terms.
|
|
|
|
This commit includes work from the past month on the T-entailment check
infrastructure (due to Tim), an entailment check for arithmetic
(also Tim), and QCF work that uses T-entailment (due to Andrew Reynolds).
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
|
|
rewrite-divk.
|
|
Short summary: By default NODEID is appeneded, just continue doing what you
were, just don't add the _$$ at the end.
Long summary:
Before this commit there were four (yes!) ways to specify the names for new
skolems, which result in names as given below
1) mkSkolem("name", ..., SKOLEM_FLAG_DEFAULT) -> "name_NODEID"
2) mkSkolem("name", ..., SKOLEM_EXACT_NAME) -> "name"
3) mkSkolem("name_$$", ..., SKOLEM_FLAG_DEFAULT) -> "name_NODEID"
4) mkSkolem("na_$$_me", ..., SKOLEM_FLAG_DEFAULT) -> "na_NODEID_me"
After this commit, only 1) and 2) stay.
90% usage is of 1) or 3), which results in exact same behavior (and
looking at the source code it doesn't look like everyone realized that
the _$$ is just redundant).
Almost no one used 4), which is the only reason to even have $$. Post this
commit if you really want a number in the middle, manually construct the
name and use the SKOLEM_EXACT_NAME flag.
|
|
Fixes an idempotency issue for non-linear multiplication with integer and real variables.
Conflicts:
src/theory/arith/normal_form.cpp
|
|
solvers.
In the process of doing this I may have fixed some bugs or some potential bugs so there
may be some user visible results of this refactoring.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
|
|
Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter.
Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up.
QCF is now functional backend to rewrite rules. Support boolean variables in QCF. Change check-model to ignore rewrite rules. Incorporate some fixes from master.
Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern.
Minor fixes to QCF/rewrite engine, removes RE on last call approach. Add option for one inst per round in RE.
Merging rewrite rules into master, check-model current fails on 3 FMF regressions.
Fix check-model issue, a line of code was omitted during merge.
|
|
non-ground ITEs also.
|
|
|
|
master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.
|
|
|
|
(resolves bug #548).
|
|
|
|
|
|
|
|
|
|
final options/logic are set.
|
|
|
|
|
|
* Rename {model,util_model}.{h,cpp} files to match class names
* Fix alreadyVisited() issue in TheoryEngine
* Remove spurious Message that causes compliance issues
* Update copyrights, fix public/private markings in headers
* minor comment fixes
* remove EXTRACT_OP as a special-case in typechecker
* note about rewriters in theoryskel readme
* Clean up some compiler warnings
* Code typos and spacing
|
|
|
|
|
