Andrew Reynolds [Tue, 10 Nov 2020 02:09:02 +0000 (20:09 -0600)]
Migrate some documentation about attributes (#5390)
From old wiki.
Andrew Reynolds [Mon, 9 Nov 2020 22:51:04 +0000 (16:51 -0600)]
Add symbol manager (#5380)
This add the symbol manager class, which is a Term-level utility, separate of the API. This class manages things like expression and assertion names, which is intentionally done outside the solver.
The symbol manager is intended to live at the same level as the Solver. When parsing input, the symbol manager will be used to model any interaction of e.g. named expressions and assertions. It also stores the symbol table of the parser.
This PR adds the basic interface for the symbol manager and passes it to the parser.
Later PRs will migrate the functionality for named expression out of e.g. SmtEngine and into SymbolManager. Commands will take Solver+SymbolManager instead of Solver. This will allow the parser to be fully migrated to the new API.
Marking "complex" since this impacts further design of the parser and the code that lives in src/main.
FYI @4tXJ7f
Andrew Reynolds [Mon, 9 Nov 2020 20:38:54 +0000 (14:38 -0600)]
Simplify handling of subtypes in smt2 printer (#5401)
This makes major simplifications to how subtypes are enforced in the smt2 printer.
It is now the principle that the smt2 prints things faithfully to the AST, regardless of whether it conforms to the smt2 standard.
It also fixes the current smt2 printing of to_real.
Conversely, this removes a hack from GetValueCommand which forced casting via x -> (/ x 1). This is now properly handled in Solver::getValue.
Some regressions change expected output as a result. Notice that internally generated Node may not conform to the smt2 standard, but user-level terms will.
Gereon Kremer [Mon, 9 Nov 2020 16:46:23 +0000 (17:46 +0100)]
Properly clear interrupt for solve() as well. (#5403)
The minisat solver stores whether it has been interrupted in asynch_interrupt and expects it to be reset before another call to solve(). MinisatSatSolver::solve() failed to do this, leading to incorrect unknown results as observed in CVC4/cvc4-projects#106. The alternative MinisatSatSolver::solve(unsigned long& resource) already did the correct thing.
Fixes CVC4/cvc4-projects#106.
Andrew Reynolds [Mon, 9 Nov 2020 13:42:03 +0000 (07:42 -0600)]
Do not regress explanations of datatype lemmas (#5376)
This modifies datatypes to not regress explanations for lemmas. This avoids segfaults in some corner cases of sygus (see attached) and leads to slightly better performance on Facebook verification benchmarks.
mudathirmahgoub [Fri, 6 Nov 2020 21:28:38 +0000 (15:28 -0600)]
Fix issue #5342 (#5349)
This PR fixes issue #5342 by adding the rewrite rule (setminus A (setminus A B)) = (intersection A B).
Andrew Reynolds [Fri, 6 Nov 2020 19:47:22 +0000 (13:47 -0600)]
(proof-new) Miscellaneous changes to strings for proofs (#5362)
This includes all minor remaining changes from proof-new for strings that were not merged to master.
This includes mostly minor changes to make proofs pass, including reordering assertions. It also removes some non-standard pedantic checks as these are now subsumed by standard ones.
It also makes the strings rewriter slightly more safe when checking arithmetic entailment under assumptions. This code used substitution, which was not safe when quantifiers were involved. This is replaced by capture avoiding substitution here.
Andrew Reynolds [Fri, 6 Nov 2020 05:06:13 +0000 (23:06 -0600)]
Split sygus template inference to its own file (#5388)
This splits techniques for inferring templates for functions-to-synthesize to their own file.
This is work towards cleaning up the single invocation utility, which will be undergoing some additions.
Andrew Reynolds [Fri, 6 Nov 2020 04:28:18 +0000 (22:28 -0600)]
Simplify printing with respect to expression types (#5394)
This removes infrastructure for stream property related to printing type annotations on all variables.
This is towards refactoring the printers.
mudathirmahgoub [Thu, 5 Nov 2020 23:13:44 +0000 (17:13 -0600)]
Remove mkSingleton from the API (#5366)
This PR removes mkSingleton from the API after removing subtyping from set theory and introducing mkInteger to the API.
Instead the user needs to use Solver::mkTerm(api::SINGLETON, element) where element has the right type.
Internally NodeManager::mkSingleton(type, element) is still needed to determine the type of the set.
Other changes:
Renamed Solver::mkTerm(Op op, .. functions to Solver::mkTermFromOp(Op op, ...
Added mkTermFromOp to the python API
Andres Noetzli [Wed, 4 Nov 2020 00:30:12 +0000 (16:30 -0800)]
Add constants from equality engine evaluation to model (#5391)
Fixes #5330. The issue mentions to related model checking failures:
When the theory of strings computes a model, there is a step that
chooses a constant that is different from other constants of the same
length in other equivalence classes. In the example, the issue was
that the constant "A" was introduced by doing evaluation in the
equality engine of the theory of strings. The constant was then not
added to the term set and was skipped while asserting the equality
engine to the theory model. As a result, an equivalence class was
assigned "A" even though it already existed, which made the model
invalid. The fix ensures that all constants in the equality engine are
added to the theory model. It should be ok to handle the issue during
model construction because other theories shouldn't have to care about
the constants that we computed internally within the theory of
strings.
When an equivalence class has a normal form that consists of a single
seq.unit, then we need to make sure that the value for the argument
is consistent with the rest of the model and we have to make sure that
we choose different values for different equivalence classes. The
commit adds code for retrieving the value of the argument to
seq.unit from the model and adds the resulting constant to the
theory model to block it for other equivalence classes. Previously,
this was not done and we ended up with two different equivalence
classes being assigned the same constant.
Andrew Reynolds [Tue, 3 Nov 2020 23:47:15 +0000 (17:47 -0600)]
Add scope methods constructing types in API (#5393)
This addresses the nightly failures. It ensures a node manager is in scope when constructing type nodes.
It also simplifies the construction of atomic type nodes to avoid an extra TypeNode(...) constructor.
Andres Noetzli [Tue, 3 Nov 2020 19:55:52 +0000 (11:55 -0800)]
Add support for printing `re.loop` and `re.^` (#5392)
In the new SMT-LIB string standard, re.loop and re.^ are indexed
operators but the printer was not updated to print them correctly. This
commit adds support for printing re.loop and re.^.
Andrew Reynolds [Tue, 3 Nov 2020 18:17:32 +0000 (12:17 -0600)]
Reset built model flag at presolve in nonlinear (#5386)
Fixes a bug in incremental with non-linear where the built model flag would still be true on the first call to check in a 2nd call to check-sat in incremental mode. This occurs when we are under the same SAT context when the model was built (likely level 0) on the subsequent check-sat call.
Fixes #5372
Andrew Reynolds [Tue, 3 Nov 2020 01:56:32 +0000 (19:56 -0600)]
Move sygus qe preproc to its own file (#5375)
makaimann [Tue, 3 Nov 2020 00:17:21 +0000 (16:17 -0800)]
Run python tests during make check (#5226)
If building with python bindings, check the pytest is installed, and adds a command to run pytest after the existing make check tests. If built without python bindings, it just uses a null command. Note: the current semantics are such that the pytest tests will not run if the ctest run fails (unless you pass the correct flag to make to continue --ignore-errors I believe). I can look into changing this semantics if that would be preferred.
Aina Niemetz [Mon, 2 Nov 2020 22:10:34 +0000 (14:10 -0800)]
contrib: Remove dependency directories. (#5367)
This automatically removes dependency directories for scripts that get
external dependencies instead of aborting with an error.
Andrew Reynolds [Mon, 2 Nov 2020 19:46:05 +0000 (13:46 -0600)]
Update strings proxy variable map to be context independent (#5377)
This makes strings proxy variables map to be context-independent. They should be context independent since we are using attributes to mark proxy variables, which are context-independent. This led to the crash reported on #5374 since proxy variables would persist across multiple user contexts, but would be missing in the user-context dependent map.
This fixes #5374.
Andrew Reynolds [Mon, 2 Nov 2020 14:26:13 +0000 (08:26 -0600)]
Miscellaneous cleaning of parser (#5369)
Andrew Reynolds [Mon, 2 Nov 2020 13:01:19 +0000 (07:01 -0600)]
Avoid dynamic allocation in symbol table implementation (#5368)
Encountered this while debugging the new symbol manager. This is not essential but probably a good idea to refactor.
Gereon Kremer [Fri, 30 Oct 2020 08:07:53 +0000 (09:07 +0100)]
Use BoundInference in nonlinear extension (#5359)
Currently the NonlinearExtensions uses a custom logic to eliminate redundant bounds and perform tightening on bound integer terms. As these replacements are not recorded, incorrect conflicts are being sent to the InferenceManager.
This PR replaces this logic by the BoundInference class and fixes the issues with conflicts by
- allowing BoundInference to collect bounds on arbitrary left hand sides (instead of only variables),
- improving origin tracking in BoundInference by explicitly constructing the new bound constraints,
- adding tightening of integer bounds,
- emitting lemmas instead of conflicts, and finally
- replacing the current logic by using the BoundInference class.
Andrew Reynolds [Fri, 30 Oct 2020 02:51:18 +0000 (21:51 -0500)]
Update api::Sort to use TypeNode instead of Type (#5363)
This is work towards removing the old API.
This makes TypeNode the backend for Sort instead of Type.
It also updates a unit test for methods isUninterpretedSortParameterized and getUninterpretedSortParamSorts whose implementation was previously buggy due to the implementation of Type-level SortType.
Andrew Reynolds [Thu, 29 Oct 2020 22:17:48 +0000 (17:17 -0500)]
Set strings pending conflict flag (#5364)
While addressing the review on
6898ab9, strings eager conflicts were accidentally disabled, this reenables them.
mudathirmahgoub [Thu, 29 Oct 2020 18:26:51 +0000 (13:26 -0500)]
Add mkInteger to the API (#5274)
This PR adds mkInteger to the API and update mkReal to ensure that the returned term has real sort.
The parsers are modified to parse numbers like "0" "5" as integers and "0.0" and "15.0" as reals.
This means subtyping is effectively eliminated from all theories except arithmetic.
Other changes:
Term::isValue is removed which was introduced to support parsing for constant arrays. It is no longer needed after this PR.
Benchmarks are updated to match the changes in the parsers
Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu
Andrew Reynolds [Thu, 29 Oct 2020 15:00:08 +0000 (10:00 -0500)]
(proof-new) Update the strings inference manager for proofs (#5220)
This updates the inference manager in strings in two ways:
(1) It now inherits from InferenceManagerBuffered, meaning that the custom methods for process the current pending lemma/fact vectors are removed in favor of the standard ones.
(2) It has support for proof generation via the InferProofCons utility.
This PR standardizes three methods processFact, processLemma, and processConflict which take InferInfo and processes any string-specific behavior pertaining to processing facts, lemmas and conflicts with the inference manager. These methods are intended to preserve the previous behavior of this class.
Gereon Kremer [Thu, 29 Oct 2020 14:25:42 +0000 (15:25 +0100)]
Add NodeManager::mkOr() (#5360)
This PR adds a convenience method mkOr() just like mkAnd().
yoni206 [Wed, 28 Oct 2020 21:52:18 +0000 (14:52 -0700)]
run_regression.py to fail on invalid requirements (#5264)
Currently, the following test is skipped when running ctest:
; REQUIRES: symfpuuuu
; EXPECT: sat
(set-logic ALL)
(assert true)
(check-sat)
I think it is better for such a test to fail, because otherwise it might never run without anyone noticing (this almost happened to me here:
c7e277b).
This PR makes such tests to fail by checking whether the REQUIRES value is valid. No regressions fail as a result.
Co-authored-by: Mathias Preiner mathias.preiner@gmail.com
Andrew Reynolds [Wed, 28 Oct 2020 21:21:53 +0000 (16:21 -0500)]
Remove more uses of Expr (#5357)
This PR removes more uses of Expr, mostly related to UnsatCore.
It makes UnsatCore a cvc4_private object storing Node instead of Expr.
Andrew Reynolds [Wed, 28 Oct 2020 20:17:05 +0000 (15:17 -0500)]
Fixes for unconstrained variables in nonlinear model (#5351)
This ensures that we explicitly mark x -> 0 as part of the arithmetic model coming from nonlinear for unconstrained variables x that nonlinear extension assumes to be 0.
This fixes #5348.
Andrew Reynolds [Wed, 28 Oct 2020 19:51:41 +0000 (14:51 -0500)]
Convert symbol table from Expr-level to Term-level (#5355)
This task is left over from parser migration.
This PR also drops support for a case of symbol overloading, in particular symbols (constructors, selectors) for parametric datatypes cannot be overloaded. One regression is disabled as a result.
Gereon Kremer [Wed, 28 Oct 2020 18:35:35 +0000 (19:35 +0100)]
Split NlSolver in multiple subsolvers (#5315)
The NlSolver started as one place for nonlinear reasoning, but has grown significantly since. This PR splits the NlSolver class into multiple smaller classes.
Andrew Reynolds [Wed, 28 Oct 2020 17:35:43 +0000 (12:35 -0500)]
Add rewrites for div/mod in the arithmetic rewriter (#5352)
This adds some basic rewrites for integer div/mod in the rewriter.
This is in preparation for improved preprocessing and rewriting for NIA problems with heavy use of div/mod.
Mathias Preiner [Tue, 27 Oct 2020 19:02:38 +0000 (12:02 -0700)]
run_regression: Add --skip-timeout option, lower timeout to 600 seconds. (#5353)
Abdalrhman Mohamed [Tue, 27 Oct 2020 18:19:11 +0000 (13:19 -0500)]
Refactor DeclareSygusVarCommand and SynthFunCommand to use the API. (#5334)
This PR is part of migrating commands. DeclareSygusVarCommand and SynthFunCommand now call public API function instead of their corresponding SmtEngine functions. Those two commands don't fully initialize the solver anymore. Some operations in SygusInterpol::solveInterpolation, which creates an interpolation sub-solver, depend on the solver being fully initialized and were affected by this change. Those operations are now executed by the main solver instead of the sub-solver, which is not fully initialized by the time they are needed.
Andrew Reynolds [Tue, 27 Oct 2020 16:46:20 +0000 (11:46 -0500)]
Add missing methods involving datatype sorts to the API (#5290)
This is required for migrating the parser's symbol table from Expr -> Term.
Gereon Kremer [Tue, 27 Oct 2020 16:16:06 +0000 (17:16 +0100)]
Disable --nl-cad option by default (#5350)
This PR disables the `--nl-cad` option by default. It was erroneously enabled with #5345 but leads to errors on, e.g., QF_NIA. Enabling for QF_NRA is done in set_defaults.
Gereon Kremer [Tue, 27 Oct 2020 12:57:55 +0000 (13:57 +0100)]
Enable --nl-cad by default (#5345)
This PR enables `--nl-cad` for QF_NRA (and QF_UFNRA) by default to improve nonlinear arithmetic solving.
Furthermore, it takes care of disabling it when libpoly is not available. It also adds a fix to the CadSolver that avoids incorrect SATs in the presence of theory combination.
mudathirmahgoub [Tue, 27 Oct 2020 01:13:23 +0000 (20:13 -0500)]
Add DUPICATE_REMOVAL operator to bags (#5336)
This PR adds duplicate removal operator to bags (also known as delta or squash).
Other changes:
print MK_BAG operator as "bag" in smt2 instead of "mkBag"
renamed BAG_IS_INCLUDED operator to SUBBAG.
Andrew Reynolds [Mon, 26 Oct 2020 17:33:01 +0000 (12:33 -0500)]
(proof-new) Add datatypes proof checker (#5340)
This adds the proof rules and proof checker for datatypes.
Andrew Reynolds [Mon, 26 Oct 2020 17:18:26 +0000 (12:18 -0500)]
Send external equalities from collapse selector as lemmas (#5346)
In
20e58d4, a policy change was made for datatypes to keep more inferences as internal facts.
This leads to a crash (issue #5344) where the equality status of two BV terms is asked by TheoryDatatypes, where the TheoryBV was not informed of the term, as datatypes kept it internal.
This refines the policy further such that the collapse selector rule is processed as a lemma for terms of external type. The reason is that this rule may generate new terms of external type. Other rules like unification retain the internal fact policy, as they do not generate new terms.
Fixes #5344.
FYI @barrettcw
mudathirmahgoub [Sat, 24 Oct 2020 14:16:52 +0000 (09:16 -0500)]
Fix issue 5271 (#5335)
This PR fixes #5271 by splitting on the equality of set members which ensures members are distinct when collectModelInfo is called.
Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu
Haniel Barbosa [Sat, 24 Oct 2020 00:20:42 +0000 (21:20 -0300)]
[proof-new] Fix n-ary kind handling in EqEngine explanations (#5332)
Adding missing cases of kinds that are n-ary but whose partial applications are
not true terms in the equality engine. This in the case not only for APPLY_UF
but also for the APPLY_* kinds for datatypes.
Andrew Reynolds [Fri, 23 Oct 2020 18:37:59 +0000 (13:37 -0500)]
Apply alpha equivalence to annotated quantified formulas (#5324)
Previously, alpha equivalence was not applied to quantified formulas with attributes, likely motivated by keeping alpha equivalent quantified formulas with different user patterns. It's not clear this is a good a idea. Moreover, this also implies that quantified formulas with user-provided names (which happens in e.g. Boogie benchmarks) also do not have alpha equivalence applied.
This makes it so that we apply alpha equivalence regardless of annotations.
FYI @barrettcw
Andrew Reynolds [Fri, 23 Oct 2020 18:24:05 +0000 (13:24 -0500)]
Change datatypes lemma policy for equalities not coming from instantiate (#5325)
Recently, the policy for lemma vs fact changed for instantiate rule in datatypes to ensure that other theories were notified of terms having external finite type. This PR further refines the policy so that the instantiate rule is the only rule whose conclusion is an equality that is sent out as a lemma.
This means that equalities from unification and collapsing selectors are always kept internal. The justification for this is that the instantiate rule is applied for all terms with the proper policy, and hence it already covers all cases where we may need to introduce new terms.
Andrew Reynolds [Fri, 23 Oct 2020 18:03:17 +0000 (13:03 -0500)]
Fix related to preregistering boolean term variables in strings (#5331)
We should only add trigger predicates for string predicates, and not arbitrary Boolean terms (which can now occur since we are handling parametric sequences).
This avoids a debug assertion failure reported on as a followup to #4370. In that benchmark BOOLEAN_TERM_VARIABLE was being added as a trigger predicate.
Gereon Kremer [Thu, 22 Oct 2020 18:06:51 +0000 (20:06 +0200)]
Use theoryof-mode=type for QF_NRA (#5326)
We've observed that our QF_NRA solving benefits significantly from --theoryof-mode=type across the board (of other options that influence QF_NRA solving). This PR sets type as the new default for QF_NRA solving.
Andrew Reynolds [Thu, 22 Oct 2020 17:24:53 +0000 (12:24 -0500)]
Remove unused equality engine types (#5319)
This is leftover from the old proof infrastructure.
mudathirmahgoub [Thu, 22 Oct 2020 16:48:25 +0000 (11:48 -0500)]
Fix issue 5309 (#5327)
This PR fixes #5309 by ensuring singleton terms are added to the model builder as representatives.
Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu
Andrew Reynolds [Thu, 22 Oct 2020 02:21:42 +0000 (21:21 -0500)]
(proof-new) Make theory preprocessor user-context dependent (#5296)
Previously, theory preprocessing cache was manually cleared whenever the theory preprocess pass was run. However, proofs for theory preprocessing required to be alive for the remainder of the user context. This PR changes theory preprocessing so that both the cache and proofs in theory preprocessing are user-context dependent.
This PR also makes the theory preprocess pass proof producing.
Gereon Kremer [Wed, 21 Oct 2020 23:19:24 +0000 (01:19 +0200)]
(proof-new) Make circuit propagator proof producing (#5318)
This PR uses the proofs from #5301 to actually produce proofs from the circuit propagator.
mudathirmahgoub [Wed, 21 Oct 2020 22:33:57 +0000 (17:33 -0500)]
Implement bags evaluator (#5322)
This PR implements NormalForm::evaluate for bags
Alex Ozdemir [Wed, 21 Oct 2020 18:53:20 +0000 (11:53 -0700)]
(proof-new) Add arith proof macros file to CMake (#5321)
Alex Ozdemir [Wed, 21 Oct 2020 18:40:02 +0000 (11:40 -0700)]
(proof-new) arith: dedup literals in flattenImpl (#5320)
TheoryArithPrivte uses flattenImplication to turn implications into
clauses. This commit ensures that said clause does not have duplicate
terms. This is important because when we write proofs related to the
clause, the proof machinery doesn't like duplicates.
Andrew Reynolds [Wed, 21 Oct 2020 14:28:38 +0000 (09:28 -0500)]
(proof-new) Updates to lazy proof chain (#5317)
Support for a default proof generator, which is optionally not called recursively.
This is required for preprocessing.
mudathirmahgoub [Wed, 21 Oct 2020 13:19:55 +0000 (08:19 -0500)]
Add operator MakeBagOp for constructing bags (#5209)
This PR removes subtyping rules for bags and add operator MakeBagOp similar to SingletonOp
Abdalrhman Mohamed [Wed, 21 Oct 2020 01:28:35 +0000 (20:28 -0500)]
Add finishInit for getInterpol and getAbduct. (#5316)
This PR removes d_subSolver from SygusInterpol class. findInterpol function now receives the sub-solver as input (possibly through solveInterpolation function). In addition, finishInit is now called for getAbduct and getInterpol functions in smt_engine.cpp.
Andrew Reynolds [Wed, 21 Oct 2020 00:12:07 +0000 (19:12 -0500)]
(proof-new) Fixes for proofs in rewriter (#5307)
This PR fixes proofs in the rewriter so that we use attributes for marking whether a node has been rewritten with proofs instead of consulting the provided TConvProofGenerator for hasRewriteStep. This additionally marks TRUST_REWRITE steps if a rewriter happens to be nondeterministic (e.g. quantifiers). It furthermore decouples rewriteWithProof from reconstruction for theory rewrite steps.
The proof postprocessor is additionally updated so that extended equality REWRITE steps are converted to THEORY_REWRITE steps with identifier RW_REWRITE_EQ_EXT for consistency, since eliminating REWRITE should result in THEORY_REWRITE only. This required generalizing the argument to THEORY_REWRITE to be a MethodId instead of a Boolean.
Aina Niemetz [Tue, 20 Oct 2020 22:06:10 +0000 (15:06 -0700)]
Fix compiler warnings. (#5305)
Gereon Kremer [Tue, 20 Oct 2020 21:32:31 +0000 (23:32 +0200)]
(proof-new) Add proofs for circuit propagator (#5301)
This PR adds code to generate proofs for inferences within the (non-clausal) circuit propagator.
It consists of many small methods that each implement simple derivations about single Boolean connectives. It uses already existing proof rules, and thus no separate proof checker is required.
A second PR will use these rules within the circuit propagator class.
Andrew Reynolds [Tue, 20 Oct 2020 21:03:00 +0000 (16:03 -0500)]
(proof-new) Fix for CDProof::isSame (#5297)
Did not check for disequalities properly.
Andrew Reynolds [Tue, 20 Oct 2020 20:20:35 +0000 (15:20 -0500)]
(proof-new) Update add lazy step interface in LazyCDProof (#5299)
Ensuring closed proofs should not be enabled by default, it is actually not used very often as a whole. Moreover, the "trust id" argument is the most useful argument and hence should come as the 3rd argument. This updates all uses of addLazyStep for the change in interface, also changes term conversion generator which had a similar issue with default arguments.
Notice that some calls to addLazyStep were checking closed but without providing a debug string, these I've left alone (they no longer check closed).
Abdalrhman Mohamed [Tue, 20 Oct 2020 19:23:30 +0000 (14:23 -0500)]
Remove some Commands from the API. (#5268)
This PR removes Solver::getAssignment command from the API as there is no way to assign names to terms in the API. It also removes ExpandDefinitionsCommand, an internal functionality in CVC4.
Andrew Reynolds [Tue, 20 Oct 2020 18:33:34 +0000 (13:33 -0500)]
Fix miscellaneous warnings (#5256)
Mostly in cardinality extension, which was cleaned in the previous PR.
Andrew Reynolds [Tue, 20 Oct 2020 16:58:37 +0000 (11:58 -0500)]
Make seq.nth a trigger kind (#5314)
This makes seq.nth a trigger kind, analogous to select in arrays.
This fixes a timeout in seq-unsolved-ematch.smt2, fixing the nightlies.
Gereon Kremer [Tue, 20 Oct 2020 15:01:30 +0000 (17:01 +0200)]
Handle rewrite to bool in BoundInference (#5311)
The BoundInference class did not properly handle rewrites that yield constant Booleans. This PR fixes this issue by explicitly checking for this case.
Andrew Reynolds [Tue, 20 Oct 2020 13:17:34 +0000 (08:17 -0500)]
Split CheckModels utility to its own file (#5303)
This utility will be undergoing major additions to make it more robust. Thus it should be moved to its own file.
There are no major code changes in this PR, a few things were changed to be consistent to the coding standard.
Aina Niemetz [Tue, 20 Oct 2020 11:41:49 +0000 (04:41 -0700)]
Integer (CLN): Minor improvements. (#5306)
Review comments by @nafur from #5304.
yoni206 [Tue, 20 Oct 2020 00:44:12 +0000 (17:44 -0700)]
Expand `seq.nth` lazily (#5287)
Our first support for seq.nth eliminated it eagerly during expandDefinitions.
This PR changes that, by eliminating it lazily, as done with other extended string operators.
Aina Niemetz [Mon, 19 Oct 2020 20:57:14 +0000 (13:57 -0700)]
Integer: CLN: Move implementation of member functions to .cpp file. (#5304)
This moves the CLN implementation of member functions of class Integer from
the header to the .cpp file. This only moves code, and adds documentation for
previously undocumented or poorly documented functions.
Analogous to #5190.
Haniel Barbosa [Mon, 19 Oct 2020 18:46:11 +0000 (15:46 -0300)]
[proof-new] Fixing resolution proof checker (#5262)
Previously the binary resolution checker was:
- Checking applications in which for a pivot (not l) the literal (not l) would be eliminated from the first clause and l from the second because double negation was handled implicitly. Now whether the binary resolution is such that the pivot is removed as is from the first clause and negated from the second, or the other way around, is marked via an argument.
- Not producing false the remaining set of literals after resolution was empty.
This commit also updates the informal description of the rule accordingly, as well as to clarify the behavior when the pivot does not occur properly in the clauses (in which case the rule application corresponds to weakening).
Co-authored-by: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Andrew Reynolds [Mon, 19 Oct 2020 17:01:33 +0000 (12:01 -0500)]
(proof-new) Updates to assertions pipeline and preprocess generator (#5300)
This updates and improves assertions pipeline and preprocess generator so that they avoid cyclic proofs and have better infrastructure for catching pedantic failures.
This is in preparation for making the non-clausal-simplification pass proof producing.
Andrew Reynolds [Mon, 19 Oct 2020 16:06:16 +0000 (11:06 -0500)]
(proof-new) Update preprocessing pass context for proofs (#5298)
This sets up the preprocessing pass context in preparation for proof production.
This PR makes the top level substitutions map into a TrustSubstitutionMap, the data structure that applies substitutions in a way that tracks proofs.
This PR also makes the "apply subst" preprocessing pass proof producing.
Haniel Barbosa [Mon, 19 Oct 2020 15:29:45 +0000 (12:29 -0300)]
[proof-new] Improving cycle checking in lazycdproofchain (#5302)
Andrew Reynolds [Mon, 19 Oct 2020 07:55:25 +0000 (02:55 -0500)]
Safer version of pending lemma processing in inference manager buffered (#5286)
This ensures we don't segfault if the pending lemma vector is cleared while we are processing it. This is potentially possible in datatypes currently. Fixes #5236.
Andrew Reynolds [Mon, 19 Oct 2020 00:58:50 +0000 (19:58 -0500)]
(proof-new) Refactoring cyclic checks (#5291)
This PR makes it so that cyclic checks are only performed eager when proofNewEagerChecking is true.
It refactors the existing cyclic check in ProofNodeToSExpr to have a more consistent style, and adds a cyclic check to getFreeAssumptions.
Andrew Reynolds [Sun, 18 Oct 2020 23:42:46 +0000 (18:42 -0500)]
(proof-new) Witness axiom reconstruction for purification skolems (#5289)
This formalizes the proofs of existentials that justify purification variables, e.g. those with witness form witness x. x = t for the term t they purify.
This PR generalizes EXISTS_INTRO to do this, and makes some simplifications to SkolemManager.
Andrew Reynolds [Sun, 18 Oct 2020 23:01:24 +0000 (18:01 -0500)]
(proof-new) Implementation of trust substitution (#5276)
Trust substitution is a data structure that is used throughout preprocessing for proofs.
This adds its implementation.
Andrew Reynolds [Sun, 18 Oct 2020 22:17:37 +0000 (17:17 -0500)]
(proof-new) More features for SMT proof post-processor (#5246)
This updates the SMT proof postprocessor with additional stats. It also adds the feature to handle conjunctions as substitution, e.g. a child proof concluding (and (= x t) (= y s)) is interpreted as a substitution for x, y, whereas previously we insisted they must be provided separately.
Andrew Reynolds [Sun, 18 Oct 2020 02:24:10 +0000 (21:24 -0500)]
(proof-new) Improvements for theory engine (#5292)
Avoids use of macro rules in a few places.
Andrew Reynolds [Fri, 16 Oct 2020 18:32:42 +0000 (13:32 -0500)]
Refactor SMT-level model object (#5277)
This refactors the SMT-level model object so that it is a wrapper around TheoryModel instead of a base class. This inheritance was unnecessary.
Moreover, it removes the virtual base models of the SMT-level model which were based on Expr. Now the interface is more minimal and in terms of Node only.
This PR further simplifies a few places in the code that interface with the SmtEngine with things related to models.
Andrew Reynolds [Fri, 16 Oct 2020 17:20:53 +0000 (12:20 -0500)]
Catch more cases of nested recursion in datatypes (#5285)
Fixes #5280.
Previously we were checking for nested recursive datatypes in expandDefinitions. This does not catch cases where the only terms of a malformed nested recursive datatype are variables. The proper place to check is in preRegisterTerm. The benchmark from that issue now gives an error.
yoni206 [Fri, 16 Oct 2020 15:04:22 +0000 (08:04 -0700)]
bv2int: caching introduced terms (#5283)
The bv-to-int preprocessing pass has a cache that maps each BV node to its translated integer node.
In case the BV node is a function symbol, it's translated integer node is a fresh function symbol.
On current master, if we later process this fresh function symbol in the preprocessing pass, we again create a fresh function symbol as its translation. This is unsound, and was discovered in #5281, whose benchmark is added to regressions.
Closes #5281 if merged.
Andrew Reynolds [Fri, 16 Oct 2020 14:17:24 +0000 (09:17 -0500)]
Add inference enumeration to datatypes (#5275)
This adds an inference enumeration for datatypes, which is analogous to what is done in strings and non-linear arithmetic. Inferences are informal identifiers that serve the purpose of (1) debugging the code, (2) providing hints on how proofs can be reconstructed.
This PR also splits the InferenceManager file in datatypes into 2.
Alex Ozdemir [Thu, 15 Oct 2020 22:27:44 +0000 (15:27 -0700)]
(proof-new) TheoryArithPrivate: farkas lemma proof (#5267)
Use a farkas proof to prove one of arithmetic's lemmas.
These changes were checked-out directly from proof-new, without modification.
mudathirmahgoub [Wed, 14 Oct 2020 23:02:27 +0000 (18:02 -0500)]
Fix issue #5269 (#5270)
This PR fixes issue #5269 of unnecessary calling TheorySetsRels::areEqual in a product relation (which compares the rightmost element of the first child with the leftmost element in the second child). This may violate an assertion in TheorySetsRels::areEqual that the types of the 2 elements should be the same
yoni206 [Wed, 14 Oct 2020 19:40:13 +0000 (12:40 -0700)]
bv2int: implementing the iand-sum mode (#5265)
There are 3 potential modes to lazily treat the iand operator:
(1) by value (typical CEGAR loop)
(2) by sum (lazily expanding each iand node into a sum of ITEs)
(3) by bit-wise equalities (lazily expanding each iand node into bit-wise equalities)
This PR implements (2).
The relevant option is added to existing tests, and a new test is added. In a few other tests, some options are removed to make them run faster.
Alex Ozdemir [Wed, 14 Oct 2020 18:37:54 +0000 (11:37 -0700)]
(proof-new) debug statements & docs for INT_TRUST (#5259)
Alex Ozdemir [Wed, 14 Oct 2020 17:17:35 +0000 (10:17 -0700)]
(proof-new) pfs in TheoryArith(Private) explainations (#5258)
Very simple, just threading the proofs through.
Andrew Reynolds [Wed, 14 Oct 2020 14:38:45 +0000 (09:38 -0500)]
Guard uses of printing approximations for constants (#5247)
Errors with these methods were encountered while working on new techniques for arithmetic preprocessing.
Also, there is obvious inefficiency since approximations for constants are being computed when certain traces are disabled.
Alex Ozdemir [Wed, 14 Oct 2020 14:00:08 +0000 (07:00 -0700)]
(proof-new) pfs for conflicts in TheoryArithPrivate (#5257)
Threads conflict proofs through TheoryArithPrivate.
Mostly just wiring things up.
yoni206 [Wed, 14 Oct 2020 06:28:36 +0000 (23:28 -0700)]
bv2int: rewritings and unsat cores (#5263)
This commit fixes several issues with bv-to-int preprocessing pass, mostly raised by @ajreynol:
1. make sure to rewrite the processed node before and after processing it
2. use the new `mkAnd` function
3. remove `--no-check-unsat-cores` from tests whenever possible
4. add new tests from #5230 . These tests now pass, and so this PR closes #5230 if merged. This also makes #5253 redundant.
5. remove an unused test
Haniel Barbosa [Wed, 14 Oct 2020 04:43:14 +0000 (01:43 -0300)]
using NOT_NOT_ELIM rather than macros to do double-neg elimination (#5261)
Alex Ozdemir [Wed, 14 Oct 2020 04:15:25 +0000 (21:15 -0700)]
(proof-new) Prove lemmas in Constraint (#5254)
Includes:
T/F splitting lemmas for any arith constraint
Unate lemmas produced early on
The hard part is proving the unate lemmas. In general, they are all implied by 2-constraint farkas proofs, so we ultimately map them all down to proveOr, which constructs that proof.
make check was happy with this change. Hopefully the CI agrees :).
Andrew Reynolds [Wed, 14 Oct 2020 03:23:38 +0000 (22:23 -0500)]
(proof-new) Generalize preprocess proof generator (#5245)
This class is of general use, not just as the overall maintainer of proofs of preprocessing, but also locally within preprocessing passes. This generalizes the interface slightly and also does some minor cleaning.
Andrew Reynolds [Wed, 14 Oct 2020 00:50:19 +0000 (19:50 -0500)]
(proof-new) Simplifications for proof rule checker interface (#5244)
Some of the interfaces in the proof rule checker are unnecessary now and can be deleted.
This also updates STRING_TRUST to have pedantic level 2.
Andrew Reynolds [Wed, 14 Oct 2020 00:10:19 +0000 (19:10 -0500)]
(proof-new) Miscellaneous minor improvements and fixes to proofs in theory files. (#5241)
Andrew Reynolds [Tue, 13 Oct 2020 23:33:57 +0000 (18:33 -0500)]
(proof-new) New rules for Booleans (#5243)
This adds 2 new rules for convenience to the Boolean checker.
Andrew Reynolds [Tue, 13 Oct 2020 22:18:02 +0000 (17:18 -0500)]
(proof-new) Change merge policy for proof node updater (#5242)
This updates the proof node updater with a mergeSubproofs field which automatically merges subproofs in the same SCOPE that prove the same thing. This is currently enabled by default, it is now configurable and disabled by default.
yoni206 [Tue, 13 Oct 2020 17:25:25 +0000 (10:25 -0700)]
bv2int: improving bvand tables (#5235)
The bv-to-int preprocessing pass introduces large ite terms that correspond to truth tables of bvand for various bit-widths.
Previously there were two inefficiencies in those tables:
They weren't being cached
The ite was not optimized
This PR adds a cache for the tables that induce the ite terms.
In addition, it computes smaller ite terms by computing the most common value of each table and using it as the default value of the ite.
Andrew Reynolds [Mon, 12 Oct 2020 22:56:32 +0000 (17:56 -0500)]
Remove uf-ss-totality option (#5251)
This option has a number of subtle bugs, it should be reimplemented if/when finite-model-find is refactored. It is not high priority enough to maintain.
This does some additional cleaning of the uf cardinality extension, some methods changed indentation.
Fixes #5239, fixes #4872, fixes #4865.