cvc5.git
3 years agoMoving methods from quantifiers engine to quantifiers state (#5881)
Andrew Reynolds [Sat, 13 Feb 2021 14:42:36 +0000 (08:42 -0600)]
Moving methods from quantifiers engine to quantifiers state (#5881)

Towards eliminating dependencies on quantifiers engine.

3 years agoProperly set up equality engine for BV bitblast solver. (#5905)
Mathias Preiner [Sat, 13 Feb 2021 14:08:37 +0000 (06:08 -0800)]
Properly set up equality engine for BV bitblast solver. (#5905)

Theory BV now sets up the default equality engine for BV solvers that do not use their own equality engine like e.g. the BV bitblast solver. This commit also adds the missing equality engine pieces to the BV bitblast solver (getEqualityStatus, explain).

3 years agoSimplify and fix decision engine's handling of skolem definitions (#5888)
Andrew Reynolds [Fri, 12 Feb 2021 09:45:29 +0000 (03:45 -0600)]
Simplify and fix decision engine's handling of skolem definitions (#5888)

This PR changes the front end of prop engine to distinguish input formulas from skolem definitions, which is required by the decision engine. This PR breaks the dependency of PropEngine on the AssertionsPipeline, as now the determining of whether an input formula is a skolem definition is handled externally, in SmtSolver.

With this PR, we should not be required to satisfy skolem definitions that are not relevant based on the techniques already implemented in the decision engine. Currently, we are not distinguishing input formulas from skolem definitions properly, meaning we assert more literals than we need to.

This also simplifies related interfaces within decision engine.

We should test this PR with --decision=justification on SMT-LIB.

3 years ago(proof-new) Option to not automatically consider symmetry in CDProof (#5895)
Andrew Reynolds [Fri, 12 Feb 2021 08:51:22 +0000 (02:51 -0600)]
(proof-new) Option to not automatically consider symmetry in CDProof (#5895)

There are compelling use cases not to automatically introduce SYMM steps in CDProof, e.g. in CDProofs used within ProofNodeUpdater for external conversions.

3 years agogoogle test: parser: Migrate parser_black. (#5886)
Aina Niemetz [Thu, 11 Feb 2021 23:34:58 +0000 (15:34 -0800)]
google test: parser: Migrate parser_black. (#5886)

3 years agoMake most methods of TheoryInferenceManager expect an InferenceId. (#5897)
Gereon Kremer [Thu, 11 Feb 2021 20:25:50 +0000 (21:25 +0100)]
Make most methods of TheoryInferenceManager expect an InferenceId. (#5897)

This PR makes most methods of the TheoryInferenceManager expect an InferenceId.
All classes that inherit from TheoryInferenceManager are adapted accordingly and InferenceIds are passed everywhere.
In some cases, there are no appropriate InferenceIds yet. We use InferenceId::UNKNOWN for the time being and introduce proper values in future PRs.
The InferenceIds are not yet used, but will be used for statistics and debug output.

3 years agoAdd InferenceId member to TheoryInference, adapt all derived classes. (#5894)
Gereon Kremer [Thu, 11 Feb 2021 19:00:18 +0000 (20:00 +0100)]
Add InferenceId member to TheoryInference, adapt all derived classes. (#5894)

This PR adds a new InferenceId member to the TheoryInference class.
All classes derived from TheoryInference are adapted accordingly.

3 years ago[proof-new] Adding a proof-producing ensure literal method (#5889)
Haniel Barbosa [Thu, 11 Feb 2021 16:13:18 +0000 (13:13 -0300)]
[proof-new] Adding a proof-producing ensure literal method (#5889)

The ensureLiteral method in CnfStream may apply CNF conversion to the given literal (for example if it's an IFF), which needs to be recorded in the proof. This commit adds a proof-producing ensureLiteral to ProofCnfStream, which is called by the prop engine if proofs are enabled.

This commit also simplifies the interfaces on ensureLit and convertAtom by removing the preRegistration flag, which was never used.

3 years agoMerge InferenceIds into one enum (#5892)
Gereon Kremer [Thu, 11 Feb 2021 14:55:31 +0000 (15:55 +0100)]
Merge InferenceIds into one enum (#5892)

This PR is the first step in consolidating the various variants of Inferences, InferenceIds and InferenceManagers of the theories.
It merges all InferencedIds into one global enum and makes all theories use them.

3 years agoFix spurious assertion failure in regexp normalization (#5852)
Andrew Reynolds [Thu, 11 Feb 2021 14:08:57 +0000 (08:08 -0600)]
Fix spurious assertion failure in regexp normalization (#5852)

Fixes #5816.

3 years agoSimplify interface for preprocessor (#5890)
Andrew Reynolds [Thu, 11 Feb 2021 13:17:53 +0000 (07:17 -0600)]
Simplify interface for preprocessor (#5890)

This does a minor simplification to the interface for preprocessor. It has a postProcess call that is called after another unrelated call at the SmtSolver level (notifyPreprocessedAssertions) is made. This makes it so that Preprocessor::postProcess is inlined as the last step of process.

3 years agoRefactor term registration visitors (#5875)
Andrew Reynolds [Wed, 10 Feb 2021 19:42:23 +0000 (13:42 -0600)]
Refactor term registration visitors (#5875)

This refactors the term registration visitors (PreRegisterVisitor and SharedTermsVisitor), which are responsible for calling Theory::preRegisterTerm and Theory::addSharedTerm.

The purpose of this PR is to resolve a subtle bug in the implementation of PreRegisterVisitor (see explanation below), and to improve performance in particular on the Facebook benchmarks (where preregistering terms is currently 25-35% of runtime on certain challenge benchmarks).

This PR makes it so that that SharedTermsVisitor now subsumes PreRegisterVisitor and should be run when sharing is enabled only. Previously, we ran both PreRegisterVisitor and SharedTermsVisitor, and moreover the former misclassified when a literal had multiple theories since the d_theories field of PreRegisterVisitor is never reset. This meant we would consider a literal to have multiple theories as soon as we saw any literal that had multipleTheories. After this PR, we run SharedTermsVisitor only which also handles calling preRegisterTerm, since it has the ability to anyways (it computes the same information as PreRegisterVisitor regarding which theories care about a term).

The refactoring merges the blocks of code that were copy and pasted in term_registration_visitor.cpp and makes them more optimal, by reducing our calls to Theory::theoryOf.

FYI @barrettcw

3 years agoFix open proof for factoring lemma (#5885)
Andrew Reynolds [Wed, 10 Feb 2021 16:27:44 +0000 (10:27 -0600)]
Fix open proof for factoring lemma (#5885)

We need to add to the current proof, regardless of whether we have used the factor skolem previously.

Fixes bugs found by @HanielB on SMT-LIB runs.

3 years agoSimplify method for inferring proxy lemmas in strings (#5789)
Andrew Reynolds [Wed, 10 Feb 2021 15:11:02 +0000 (09:11 -0600)]
Simplify method for inferring proxy lemmas in strings (#5789)

This PR simplifies our heuristic for inferring when an explanation for a strings lemma can be minimized based on proxy variable definitions. In particular, we do not turn solved equalities for proxy variables into substitutions. This aspect of the heuristic is incompatible with the new eager solver work, and moreover is buggy since substitutions should not be applied within string terms. The latter was leading the incorrect models on the 2 issues fixed by this PR.

Current results on the eager solver on SMT-LIB shows this change has very little performance impact.

Fixes #5692, fixes #5610.

3 years agoRemove track instantiations infrastructure (#5883)
Andrew Reynolds [Wed, 10 Feb 2021 02:43:59 +0000 (20:43 -0600)]
Remove track instantiations infrastructure (#5883)

This was used in the old method for unsat core tracking for instantiation lemmas, which will soon be subsumed.

This is also work towards eliminating the dependencies on quantifiers engine from Instantiate.

3 years agoOptimize get skolems method (#5876)
Andrew Reynolds [Wed, 10 Feb 2021 02:07:33 +0000 (20:07 -0600)]
Optimize get skolems method (#5876)

This method is used to determine which skolems have definitions according to term formula removal. This optimizes the method using attributes similar to how expr::getFreeVariables works.

It will be used heavily for SAT relevancy. We should also consider updating the justification heuristic to use this method.

3 years agoDo not traverse quantifiers in term formula removal (#5859)
Andrew Reynolds [Wed, 10 Feb 2021 00:21:56 +0000 (18:21 -0600)]
Do not traverse quantifiers in term formula removal (#5859)

Our current policy for term formula removal leaves quantifier bodies unchanged. This simplifies the code based on this observation.

3 years agocmake: Make Python3 default and improve toml error messages. (#5884)
Mathias Preiner [Tue, 9 Feb 2021 23:18:14 +0000 (15:18 -0800)]
cmake: Make Python3 default and improve toml error messages. (#5884)

./configure.sh will now fail if Python3 is not installed on the system. Since Python2 is now deprecated the user has to explicitly enable it via --python2. This commit also removes the --python3 configure flag.

3 years agoEliminating dependencies from inst utils (#5882)
Andrew Reynolds [Tue, 9 Feb 2021 22:09:54 +0000 (16:09 -0600)]
Eliminating dependencies from inst utils (#5882)

Towards eliminating dependence on QuantifierEngine from inst_match_trie.

3 years agoMake term database optionally SAT-context-dependent (#5877)
Andrew Reynolds [Tue, 9 Feb 2021 21:35:40 +0000 (15:35 -0600)]
Make term database optionally SAT-context-dependent (#5877)

This makes the terms registered to the term database (those considered by E-matching) optionally stored in a SAT-context-dependent manner. The motivation is to have a more flexible/fine-grained set of terms considered by E-matching, e.g. if preregistration becomes lazier in the future.

This uncovered 2 issues:

The induction techniques in "conjecture generator" were using private interfaces, this PR removes the friend relaionship and cleans the code
The conflict-based instantiation module was accessing the signature tables for BOUND_VARIABLES when an operator of an APPLY_UF was a BOUND_VARIABLE. This is possible when options::ufHo is enabled. This makes conflict-based instantiation skip such terms.

3 years agogoogle test: expr: Migrate node_manager_black. (#5857)
Aina Niemetz [Tue, 9 Feb 2021 20:04:13 +0000 (12:04 -0800)]
google test: expr: Migrate node_manager_black. (#5857)

3 years agogoogle test: main: Migrate interactive_shell_black. (#5878)
Aina Niemetz [Tue, 9 Feb 2021 18:40:06 +0000 (10:40 -0800)]
google test: main: Migrate interactive_shell_black. (#5878)

3 years agogoogle test: expr: Migrate type_cardinality_black. (#5871)
Aina Niemetz [Tue, 9 Feb 2021 17:47:53 +0000 (09:47 -0800)]
google test: expr: Migrate type_cardinality_black. (#5871)

3 years agogoogle test: expr: Migrate node_self_iterator_black. (#5865)
Aina Niemetz [Tue, 9 Feb 2021 16:01:29 +0000 (08:01 -0800)]
google test: expr: Migrate node_self_iterator_black. (#5865)

3 years ago[quantifiers] Fix prenex computation (#5879)
Haniel Barbosa [Tue, 9 Feb 2021 03:37:10 +0000 (00:37 -0300)]
[quantifiers] Fix prenex computation (#5879)

Previously our prenex computation could generate quantifiers of the form forall x y y. F, which would lead to an assertion failure in getFreeVariablesScope, as it assumes that no shadowing occurs. This commit makes the prenex computation take a set rather than a vector, thus avoiding duplications of prenexed variables. It also changes mkForall to take a constant vector, since it does not modify the given vector.

Fixes #5693

3 years agogoogle test: expr: Migrate type_node_white. (#5872)
Aina Niemetz [Tue, 9 Feb 2021 01:44:21 +0000 (17:44 -0800)]
google test: expr: Migrate type_node_white. (#5872)

3 years agoUse quantifiers inference manager for lemma management (#5867)
Andrew Reynolds [Mon, 8 Feb 2021 22:50:16 +0000 (16:50 -0600)]
Use quantifiers inference manager for lemma management (#5867)

Towards eliminating dependencies on quantifiers engine.

This replaces the custom implementation of lemma management in quantifiers engine with the standard one.

It makes a few minor changes to the standard inference manager classes to ensure the same behavior for quantifiers.

Note that some minor changes in behavior are introduced in this PR, such as being more consistent about caching/rewriting lemmas. This should not have any major impact.

3 years agoFix disequality between seq.unit terms (#5880)
Andrew Reynolds [Mon, 8 Feb 2021 21:55:32 +0000 (15:55 -0600)]
Fix disequality between seq.unit terms (#5880)

This adds a missing inference for disequality between seq.unit terms, which was not handled previously.

Fixes #5666.

3 years agogoogle test: expr: Migrate node_white. (#5869)
Aina Niemetz [Mon, 8 Feb 2021 20:03:05 +0000 (12:03 -0800)]
google test: expr: Migrate node_white. (#5869)

3 years agoFix dumping of assertions for monolithic preprocessing passes (#5866)
Haniel Barbosa [Mon, 8 Feb 2021 19:32:18 +0000 (16:32 -0300)]
Fix dumping of assertions for monolithic preprocessing passes (#5866)

Previously we were unable to dump assertions in ProcessAssertions::apply for the definition-expansion, simplify and repeat-simplify passes.

3 years agoRemove support for inst closure (#5874)
Andrew Reynolds [Mon, 8 Feb 2021 18:29:58 +0000 (12:29 -0600)]
Remove support for inst closure (#5874)

This was a feature implemented for "Deciding Local Theory Extensions via E-matching" CAV 2015 that is not used anymore, and will be a burden to maintain further with potential changes to term database.

It also simplifies the TermDatabase::addTerm method (which changed indentation).

3 years agoUse consistent names for fixtures in unit tests. (#5863)
Aina Niemetz [Mon, 8 Feb 2021 17:55:38 +0000 (09:55 -0800)]
Use consistent names for fixtures in unit tests. (#5863)

3 years agogoogle test: expr: Migrate node_traversal_black. (#5868)
Aina Niemetz [Mon, 8 Feb 2021 17:26:32 +0000 (09:26 -0800)]
google test: expr: Migrate node_traversal_black. (#5868)

3 years agoAvoid spurious traversal of terms during preregistration (#5860)
Andrew Reynolds [Mon, 8 Feb 2021 15:17:31 +0000 (09:17 -0600)]
Avoid spurious traversal of terms during preregistration (#5860)

This simplifies a few places in the code which unecessarily traverse terms during preregistration (which already traverses terms).

3 years agoDo not combine theories if theory engine needs check (#5861)
Andrew Reynolds [Sat, 6 Feb 2021 01:14:01 +0000 (19:14 -0600)]
Do not combine theories if theory engine needs check (#5861)

In rare cases, theory combination would be run when theory engine still needs check. This was limited to cases where the output channel is used but no lemmas were sent (TheoryEngine::needCheck() vs. d_lemmasAdded).

This led to problems in the theory of sets, which does not run a full effort check if theory engine needs check (since it knows it will be called to check again). However, running theory combination in these cases is not safe since theory of sets computes information pertaining to the care graph during its full effort check. Running theory combination otherwise would lead to theory of sets using stale data, leading to crashes due to terms not appearing in the equality engine.

This fixes #4124 (which appears not to trigger on master anyways currently).

This bug has also appeared on my sat relevancy development branch, hence fixing on master.

3 years agogoogle test: expr: Migrate symbol_table_black. (#5870)
Aina Niemetz [Fri, 5 Feb 2021 22:32:33 +0000 (14:32 -0800)]
google test: expr: Migrate symbol_table_black. (#5870)

3 years agoMinor cleaning of quantifiers engine (#5858)
Andrew Reynolds [Fri, 5 Feb 2021 20:53:47 +0000 (14:53 -0600)]
Minor cleaning of quantifiers engine (#5858)

This member is currently unused.

3 years agogoogle test: expr: Migrate node_manager_white. (#5864)
Aina Niemetz [Fri, 5 Feb 2021 20:11:54 +0000 (12:11 -0800)]
google test: expr: Migrate node_manager_white. (#5864)

3 years agoRemove obsolete include from node_black unit test. (#5862)
Aina Niemetz [Fri, 5 Feb 2021 19:36:32 +0000 (11:36 -0800)]
Remove obsolete include from node_black unit test. (#5862)

3 years agogoogle test: expr: Migrate node_builder_black. (#5855)
Aina Niemetz [Fri, 5 Feb 2021 17:20:46 +0000 (09:20 -0800)]
google test: expr: Migrate node_builder_black. (#5855)

3 years agoMiscellaneous cleaning in theory engine (#5854)
Andrew Reynolds [Fri, 5 Feb 2021 16:04:30 +0000 (10:04 -0600)]
Miscellaneous cleaning in theory engine (#5854)

This statistic is unused, I believe it is leftover from deleted code.

3 years agoAdding an option to optimize polite combination for datatypes (#5856)
yoni206 [Thu, 4 Feb 2021 23:46:12 +0000 (15:46 -0800)]
Adding an option to optimize polite combination for datatypes (#5856)

This PR makes the optimization introduced in bbca987 optional.

3 years agoIntroduce quantifiers registry utility (#5829)
Andrew Reynolds [Thu, 4 Feb 2021 22:55:00 +0000 (16:55 -0600)]
Introduce quantifiers registry utility (#5829)

This is a simple module for determining which quantifiers module has ownership of quantified formulas.

This is work towards eliminating dependencies of quantifiers modules.

Note that quantifiers attributes module (which no longer has a dependency on QuantifiersEngine after this PR) will be embedded into this module in a later PR.

3 years agoClarifying documentation of `--static-binary` (#5844)
yoni206 [Thu, 4 Feb 2021 21:58:38 +0000 (13:58 -0800)]
Clarifying documentation of `--static-binary` (#5844)

The documentation regarding --static-binary is improved.

3 years agoEliminate equality query dependence on quantifiers engine (#5831)
Andrew Reynolds [Thu, 4 Feb 2021 21:18:05 +0000 (15:18 -0600)]
Eliminate equality query dependence on quantifiers engine (#5831)

This class will be renamed "RepSelector" on a future PR. It no longer needs to depend on quantifiers engine and can be initialized after the modules it depends on.

3 years ago[proof-new] Catch trivial cycles in SAT proof generation (#5853)
Haniel Barbosa [Thu, 4 Feb 2021 14:59:56 +0000 (11:59 -0300)]
[proof-new] Catch trivial cycles in SAT proof generation (#5853)

Evaluating the proof infrastructure in SMT-LIB has uncovered a rare
case (i.e., not previously in our regressions!!) in which we generate
a trivial cycle during SAT proof generation, which can lead to
problematic cycles when expanding MACRO_RESOLUTION steps. For example,
we can go from

       l1 v l2   ~l1 v l3   ~l2 v l3
(ok) ------------------------------
                  l3
in which l3 = l1 v l2, to

         l1 v l2   ~l1 v l3   ~l2 v l3
(bad) ------------------------------
               l3 v l3
              ---------
                 l3
This commit now catches the trivial cycle before it's generated.

3 years agoAdd BV solver bitblast. (#5851)
Mathias Preiner [Wed, 3 Feb 2021 20:38:09 +0000 (12:38 -0800)]
Add BV solver bitblast. (#5851)

This PR adds a new bit-blasting BV solver, which can be enabled via --bv-solver=bitblast. The new bit-blast solver can be used instead of the lazy BV solver and currently supports CaDiCaL and CryptoMiniSat as SAT back end.

3 years ago[proof-new] Fix MACRO_RESOLUTION expansion for singleton clause corner case (#5850)
Haniel Barbosa [Wed, 3 Feb 2021 15:11:26 +0000 (12:11 -0300)]
[proof-new] Fix MACRO_RESOLUTION expansion for singleton clause corner case (#5850)

Evaluating the proof infrastructure in SMT-LIB has uncovered a rare case (i.e., not previously in our regressions!!) in which the resulting clause from crowding literal elimination is a singleton. This commit makes the expansion code robust to that and adds an example of a problematic benchmark as a regression.

Also improves a bit tracing and some comments.

3 years ago(proof-new) Miscellaneous fixes and regressions (#5841)
Andrew Reynolds [Tue, 2 Feb 2021 21:12:45 +0000 (15:12 -0600)]
(proof-new) Miscellaneous fixes and regressions (#5841)

3 years ago(proof-new) Refactor theory preprocessing (#5835)
Andrew Reynolds [Tue, 2 Feb 2021 20:48:59 +0000 (14:48 -0600)]
(proof-new) Refactor theory preprocessing (#5835)

This simplifies our algorithm for theory preprocessing. The motivation is two-fold:
(1) Proofs are currently incorrect in rare cases due to incorrectly tracking pre vs post rewrites.
(2) We can avoid traversing Boolean connectives with term formula removal. Note that this PR relies on the observation that term formula removal leaves Boolean structure unchanged and can apply locally to theory atoms.

Furthermore, notice that our handling of lemmas generated by term formula removal is now more uniform. In the second algorithm, term formula removal is not applied to fixed point anymore. In other words, we do not remove skolems from lemmas generated by term formula removal recursively. Instead, since lemmas are theory-preprocessed recursively, we use the fixed point that runs outside the above algorithm instead of relying on the inner fixed point in term formula removal.

This PR resolves several open issues with proof production on proof-new.

I will performance test this change on SMT-LIB.

3 years agoRemove quantifiers regression from decision folder (#5830)
Andrew Reynolds [Tue, 2 Feb 2021 20:20:44 +0000 (14:20 -0600)]
Remove quantifiers regression from decision folder (#5830)

This is a duplicate of https://github.com/CVC4/CVC4/blob/master/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 and moreover is slow on proof-new.

3 years agoCleanup some includes (#5847)
Andrew Reynolds [Tue, 2 Feb 2021 18:25:21 +0000 (12:25 -0600)]
Cleanup some includes (#5847)

In particular, theory_engine.h is included many places spuriously.

A few blocks of code changed indentation, updated to guidelines.

3 years agoImprovements for NL traces (#5846)
Andrew Reynolds [Tue, 2 Feb 2021 15:49:25 +0000 (09:49 -0600)]
Improvements for NL traces (#5846)

This makes it so that -t nl-ext is a concise summary of what the nl-ext solver is doing, which I use frequently for debugging.

This is a temporary solution, we should consider a deeper refactoring of traces throughout NL at some point.

3 years ago[proof-new] Fix bug in expansion of MACRO_RESOLUTION (#5845)
Haniel Barbosa [Tue, 2 Feb 2021 14:17:33 +0000 (11:17 -0300)]
[proof-new] Fix bug in expansion of MACRO_RESOLUTION (#5845)

Evaluating the proof infrastructure in SMT-LIB has uncovered a rare case (i.e., not previously in our regressions!!) in which a crowding literal occurs in an OR node that represents a single-literal clause subsequent to the last clause that includes the crowding literal. This was leading to the clause that eliminates the crowding literal not being found. The commit fixes this issue by excluding single-literal clauses from those that can introduce crowding literals (which was already marked as necessary but not properly enforced).

3 years agoEliminate PREPROCESS lemma property (#5827)
Andrew Reynolds [Mon, 1 Feb 2021 20:55:19 +0000 (14:55 -0600)]
Eliminate PREPROCESS lemma property (#5827)

This is now possible since we always preprocess lemmas.

Note that the LemmaProperty on inferences may be redundant throughout the non-linear solver now.

3 years agoSimplify alpha equivalence module (#5839)
Andrew Reynolds [Mon, 1 Feb 2021 19:58:14 +0000 (13:58 -0600)]
Simplify alpha equivalence module (#5839)

This class uses a discrimination tree which can compute subsumption as well as alpha-equivalence. This class was initially designed to also support subsumption. However, we were only using this class for alpha-equivalence and hence (canonized) Node comparison suffices and the class can be simplified. It also makes minor cosmetic updates to the module.

If we plan to support subsumption checking later, we will write a new module, and use this class https://github.com/CVC4/CVC4/blob/master/src/expr/match_trie.h which is a more mature version of the class deleted by this PR.

Note: I verified that the new and old implementation was equivalent using a temporary AlwaysAssert.

3 years agoAvoid calling the printers while converting sexpr to string. (#5842)
Abdalrhman Mohamed [Mon, 1 Feb 2021 18:40:58 +0000 (12:40 -0600)]
Avoid calling the printers while converting sexpr to string. (#5842)

This PR modifies sexprToString to use Term::getString to get string constants instead of Term::toString, which depends on the output language. The previous behavior caused CVC4 to crash when AST is picked as the output language.

3 years agoFix BagsRewriter::rewriteUnionDisjoint (#5840)
mudathirmahgoub [Mon, 1 Feb 2021 14:42:39 +0000 (08:42 -0600)]
Fix BagsRewriter::rewriteUnionDisjoint (#5840)

This PR fixes the implementation of (union_disjoint (union_max A B) (intersection_min A B)) =(union_disjoint A B).
It also skips processed bags during model building.

3 years agoFix unguarded call to get representative (#5838)
Andrew Reynolds [Sat, 30 Jan 2021 22:25:08 +0000 (16:25 -0600)]
Fix unguarded call to get representative (#5838)

Introduced in 3234db4.
Fixes #5837, that benchmark is now unknown.
Adds an SMT-LIB benchmark that also crashes.

3 years ago[proof-new] Connecting new unsat cores (#5834)
Haniel Barbosa [Fri, 29 Jan 2021 22:34:57 +0000 (19:34 -0300)]
[proof-new] Connecting new unsat cores (#5834)

Allows one to generate unsat cores from the new proof infrastructure. For new this is controlled by a new option, --check-unsat-cores-new.

3 years agoAdd bag inferences for operators: intersection, duplicate_removal, and empty bags...
mudathirmahgoub [Fri, 29 Jan 2021 21:44:28 +0000 (15:44 -0600)]
Add bag inferences for operators: intersection, duplicate_removal, and empty bags (#5832)

This PR adds inferences for operators: intersection, duplicate_removal, and empty bags during post check.
It also fixes a bug in SolverState::getElements

3 years ago(proof-new) Distinguish pre vs post rewrites in term conversion proof generator ...
Andrew Reynolds [Fri, 29 Jan 2021 19:27:44 +0000 (13:27 -0600)]
(proof-new) Distinguish pre vs post rewrites in term conversion proof generator (#5833)

This is work towards resolving two kinds of failures on proof-new:

(1) Functional issues with proofs from the rewriter, in particular when a term pre-rewrites and post-rewrites to different things,
(2) Conversion issues in theory-preprocessing, where all steps are assumed to be post-rewrites but some are in fact pre-rewrites. This leads to the term conversion proof generator proving something different than what is expected.

A followup PR will simplify and fix proofs for theory-preprocessing.

3 years agoReorganize calls to quantifiers engine from SmtEngine layer (#5828)
Andrew Reynolds [Thu, 28 Jan 2021 21:58:17 +0000 (15:58 -0600)]
Reorganize calls to quantifiers engine from SmtEngine layer (#5828)

This reorganizes calls to QuantifiersEngine from SmtEngine. Our policy has changed recently that the SmtEngine layer is allowed to make calls directly to QuantifiersEngine, which eliminates the need for TheoryEngine to have forwarding calls. This PR makes this policy more consistent.

This also makes quantifier-specific calls more safe by throwing modal exceptions in the cases where quantifiers are present.

Marking "major" since we currently segfault when e.g. dumping instantiations in non-quantified logics. This PR makes it so that we throw a modal exception.

3 years agoRemove regex header from cvc4cpp.cpp (#5826)
mudathirmahgoub [Thu, 28 Jan 2021 20:51:28 +0000 (14:51 -0600)]
Remove regex header from cvc4cpp.cpp (#5826)

This PR replaces the heavy hammer std::regex_match for checking numbers with string operations

3 years agoSimplify lemma interface (#5819)
Andrew Reynolds [Thu, 28 Jan 2021 20:01:26 +0000 (14:01 -0600)]
Simplify lemma interface (#5819)

This makes it so that TheoryEngine::lemma returns void not LemmaStatus.

Currently, there was only one use of LemmaStatus by theory solvers, which was CEGQI using it as a way of getting the preprocessed form of a lemma. This makes it so that there is an explicit method in Valuation for getting the preprocessed form of a term + its skolems and their definition assertions.

It also simplifies a few things, e.g. Valuation calls are forwarded to PropEngine instead of going through TheoryEngine. It fixes a few issues in TermFormulaRemoval related to getSkolems.

3 years agoUse standard equality engine information in quantifiers state (#5824)
Andrew Reynolds [Thu, 28 Jan 2021 19:27:27 +0000 (13:27 -0600)]
Use standard equality engine information in quantifiers state (#5824)

This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState.

This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.

3 years agoAlways theory-preprocess lemmas (#5817)
Andrew Reynolds [Thu, 28 Jan 2021 14:25:38 +0000 (08:25 -0600)]
Always theory-preprocess lemmas (#5817)

This PR makes it so that theory-preprocessing is always called on lemmas. It simplifies the proof production in the theory preprocessor accordingly.

Additionally, it ensures that our theory-preprocessor is run on lemmas that are generated from term formula removal. Previously, this was not the case and in fact certain lemmas (e.g. literals within witness terms that are not in preprocessed form) would escape and be asserted to TheoryEngine. This was uncovered by a unit test failure, the corresponding regression is added in this PR.

It adds a new interface removeItes to PropEngine which is required for the (deprecated) preprocessing pass removeItes.

This PR now makes the lemma propery PREPROCESS obsolete. Further simplification is possible after this PR in non-linear arithmetic and quantifiers, where it is not necessary to distinguish 2 caches for preprocessed vs. non-preprocessed lemmas.

3 years agoAdd option for whether to filter candidate rewrite pairs (#5825)
Andrew Reynolds [Wed, 27 Jan 2021 20:37:41 +0000 (14:37 -0600)]
Add option for whether to filter candidate rewrite pairs (#5825)

This option should be disabled for the new sygus reconstruction algorithm on #5779.

3 years agoSplit pattern term selector from trigger (#5811)
Andrew Reynolds [Wed, 27 Jan 2021 19:04:46 +0000 (13:04 -0600)]
Split pattern term selector from trigger (#5811)

This separates the utilities for selecting pattern terms from the Trigger class itself. This includes a PatternTermSelector, which implements the techniques for selecting the pool of pattern terms, and TriggerTermInfo which contains basic information about pattern terms.

It makes minor refactoring to make the PatternTermSelector class more than just static methods, e.g. it is now a configurable object that selects pattern terms. This makes some of the methods take fewer arguments.

More refactoring is possible, to be addressed on future PRs.

3 years ago(proof-new) Improvements to quantifiers engine and instantiate interfaces (#5814)
Andrew Reynolds [Wed, 27 Jan 2021 16:32:32 +0000 (10:32 -0600)]
(proof-new) Improvements to quantifiers engine and instantiate interfaces (#5814)

This makes printing instantiations done at the SmtEngine level instead of deeply embedded within the Instantiate module. This provides much better flexibility for future uses of instantiations (e.g. how they are minimized in the new proof infrastructure).

Note this PR breaks the functionality that instantiations are minimized based on the old unsat cores infrastructure (see the disabled regression). This will be fixed once proof-new is fully merged.

3 years agoThread proofs through arith channels & similar (#5818)
Alex Ozdemir [Wed, 27 Jan 2021 03:20:32 +0000 (19:20 -0800)]
Thread proofs through arith channels & similar (#5818)

Thread proofs through conflict/lemma storages & channels in TheoryArithPrivate

d_acTmp
d_approxCuts
lemma output channel
conflict output channel

3 years agoUse term canonizer utility locally in quantifiers (#5823)
Andrew Reynolds [Wed, 27 Jan 2021 02:45:26 +0000 (20:45 -0600)]
Use term canonizer utility locally in quantifiers (#5823)

Term canonization was used in two places, which are unrelated and don't need to share the instance.
Also removes a few unnecessary methods from QuantifiersEngine.

3 years agoUse standard conflict mechanism in quantifiers state (#5822)
Andrew Reynolds [Wed, 27 Jan 2021 01:24:58 +0000 (19:24 -0600)]
Use standard conflict mechanism in quantifiers state (#5822)

Work towards eliminating dependencies on quantifiers engine, this updates quantifiers module to use the standard SAT-context dependent flag in quantifiers state instead of the one in QuantifiersEngine. It also eliminates the use of a custom call to theoryEngineNeedsCheck.

3 years agoIntroduce quantifiers inference manager (#5821)
Andrew Reynolds [Tue, 26 Jan 2021 21:03:23 +0000 (15:03 -0600)]
Introduce quantifiers inference manager (#5821)

This is the second prerequisite for eliminating dependencies on quantifiers engine. This PR threads a quantifiers inference manager through all modules in quantifiers that add lemmas.

The code for adding lemmas in quantifiers engine will be migrated to this class.

3 years agoRemove deprecated quantifiers modules (#5820)
Andrew Reynolds [Tue, 26 Jan 2021 20:11:10 +0000 (14:11 -0600)]
Remove deprecated quantifiers modules (#5820)

3 years agoRefactor quantifiers engine initialization (#5813)
Andrew Reynolds [Tue, 26 Jan 2021 18:43:50 +0000 (12:43 -0600)]
Refactor quantifiers engine initialization (#5813)

This is a step towards breaking up the quantifiers engine.

The key change is that QuantifiersEngine will not be passed as a pointer to the modules it contains. This PR makes it so that necessary modules take a QuantifiersState, which will eventually be extended as needed with additional query methods. For now, modules will take both until the dependencies on QuantifersEngine are removed.

This required that QuantifiersEngine now lives in TheoryQuantifiers, instead of in TheoryEngine, since the QuantifiersEngine must be initialized with QuantifiersState, which is a member of TheoryQuantifiers. Now, TheoryEngine retrieves the QuantifiersEngine from TheoryQuantifiers prior to finishing initialization on theories.

3 years agoReestablishing support for define-sort (#5810)
Haniel Barbosa [Tue, 26 Jan 2021 16:10:33 +0000 (13:10 -0300)]
Reestablishing support for define-sort (#5810)

Presumable broken since 3ed42d7ab. This extends the API to have a substitute method for Sort that in needed for doing the Sort substitution in the case of define-sort.

This fixes issue #5809.

3 years agoAdd proofs to TheoryArithPrivate::propagate (#5812)
Alex Ozdemir [Tue, 26 Jan 2021 04:20:58 +0000 (20:20 -0800)]
Add proofs to TheoryArithPrivate::propagate (#5812)

Specifically, add proofs to conflicts between (a) a propagation from the
congruence manager and (b) a constraint from the main solver.

3 years agoRefactor bags::SolverState (#5783)
mudathirmahgoub [Mon, 25 Jan 2021 20:38:45 +0000 (14:38 -0600)]
Refactor bags::SolverState (#5783)

Couple of changes:

SolverState now keep tracks of elements per bag instead of per type.
bags::InferInfo now stores multiple conclusions (conjuncts).
BagSolver applies upward/downward closures for bag elements

3 years agoEnsure uses of ground terms in triggers are preprocessed and registered (#5808)
Andrew Reynolds [Mon, 25 Jan 2021 17:11:02 +0000 (11:11 -0600)]
Ensure uses of ground terms in triggers are preprocessed and registered (#5808)

This ensures ground terms in triggers are preprocessed and registered in the master equality engine. This avoids cases where our E-matching algorithm is incomplete where it should not be.

Positive impact (+222-69) on SMT-LIB, 30 second timeout

3 years agoSplit inst match generator into multiple files (#5805)
Andrew Reynolds [Mon, 25 Jan 2021 16:29:39 +0000 (10:29 -0600)]
Split inst match generator into multiple files (#5805)

No code changes on this PR, only move + format.

3 years agoSplit E-matching strategies to own files (#5807)
Andrew Reynolds [Mon, 25 Jan 2021 14:59:18 +0000 (08:59 -0600)]
Split E-matching strategies to own files (#5807)

Code move + format only

3 years agorename InferInfo::d_newSkolem to InferInfo::d_skolems (#5799)
mudathirmahgoub [Mon, 25 Jan 2021 00:18:12 +0000 (18:18 -0600)]
rename InferInfo::d_newSkolem to InferInfo::d_skolems (#5799)

Rename strings::InferInfo::d_newSkolem to InferInfo::d_skolems to match bags::InferInfo:d_skolems

3 years ago Initial cleaning of e-matching instantiation strategy (#5796)
Andrew Reynolds [Sun, 24 Jan 2021 19:55:50 +0000 (13:55 -0600)]
 Initial cleaning of e-matching instantiation strategy (#5796)

In preparation for splitting this into multiple files.

No behavior changes in this PR.

3 years agoInitial cleaning of triggers (#5795)
Andrew Reynolds [Sun, 24 Jan 2021 19:13:06 +0000 (13:13 -0600)]
Initial cleaning of triggers (#5795)

In preparation for splitting trigger.h/cpp into multiple files.

This updates the code to conform to guidelines. No major changes, apart from a heuristic related to "pure theory triggers" is deleted and simplified.

3 years agoInitial cleaning of inst match generator (#5794)
Andrew Reynolds [Sun, 24 Jan 2021 18:43:54 +0000 (12:43 -0600)]
Initial cleaning of inst match generator (#5794)

In preparation towards breaking this file up into multiple files.

No code changes, only updates to conform to new guidelines.

3 years ago(proof-new) Instantiation list utility (#5768)
Andrew Reynolds [Sun, 24 Jan 2021 18:12:10 +0000 (12:12 -0600)]
(proof-new) Instantiation list utility (#5768)

This is in preparation for refactoring the printing of instantiations. We will migrate the printing of instantiations (currently done in the Instantiate module within quantifiers engine) to somewhere more high level e.g. the SmtEngine or in the command layer. This will make the infrastructure for dumping instantiations much more flexible, as implemented on proof-new.

3 years agoAdd interface for getting preprocessed term (#5798)
Andrew Reynolds [Sun, 24 Jan 2021 17:42:08 +0000 (11:42 -0600)]
Add interface for getting preprocessed term (#5798)

Several places, e.g. in quantifiers, requiring knowing what the theory-preprocessed form of a node is.

This is required for an improvement to our E-matching algorithm, which requires knowing what the preprocessed form of ground subterms of triggers are.

Note that I'm not 100% happy with adding a new interface to Valuation, but at the moment I don't see a better way of doing this. On the positive side, this interface will make a few other things (e.g. the return value of OutputChannel::lemma) obsolete.

3 years ago[proof-new] Expanding MACRO_RESOLUTION in post-processing (#5755)
Haniel Barbosa [Fri, 22 Jan 2021 16:15:43 +0000 (13:15 -0300)]
[proof-new] Expanding MACRO_RESOLUTION in post-processing (#5755)

Breaks down resolution, factoring and reordering. The hardest part of this process is making getting rid of the so-called "crowding literals", i.e., duplicate literals introduced during the series of resolutions and removed implicitly by the SAT solver. A naive removal via addition of premises to the chain resolution can lead to exponential behavior, so instead the removal is done by breaking the resolution and applying a factoring step midway through. This guarantees non-exponential behavior.

3 years agoAdd div, mod, abs in non-strict parsing mode (#5793)
Andrew Reynolds [Thu, 21 Jan 2021 18:07:50 +0000 (12:07 -0600)]
Add div, mod, abs in non-strict parsing mode (#5793)

The recent change to the parser currently breaks our performance on several critical applications, including the use of CVC4 in Facebook. We should only throw a parse error for div in linear logics when strict mode is enabled.

3 years agoarith: Proofs for Diophantine cuts (#5792)
Alex Ozdemir [Thu, 21 Jan 2021 04:30:56 +0000 (20:30 -0800)]
arith: Proofs for Diophantine cuts (#5792)

Thread proofs through the diophantine "cutting" lemma generator.

3 years agoRefactoring the single invocation solver (#5706)
Andrew Reynolds [Wed, 20 Jan 2021 23:32:06 +0000 (17:32 -0600)]
Refactoring the single invocation solver (#5706)

This does an intermediate refactoring of the single invocation solver to make a few things clearer and to add preliminary support for functions that have been marked as solved by external techniques.

This is in preparation for generalizing the CAV 2015 single invocation techniques.

3 years agoFix type issues with relevant domain computation (#5788)
Andrew Reynolds [Wed, 20 Jan 2021 21:56:26 +0000 (15:56 -0600)]
Fix type issues with relevant domain computation (#5788)

This fixes 2 issues with relevant domain type computation, the first involving arithmetic INST_CONSTANT that do not belong to the current quantified formula being solved for in a monomial sum, the second involving parametric datatype selectors.

Fixes #5635. Both benchmarks on that issue are unsolved (one timeout, one unknown) but throw no assertion failure.

3 years agoFix corner case of wrongly applied selector as trigger (#5786)
Andrew Reynolds [Wed, 20 Jan 2021 18:59:13 +0000 (12:59 -0600)]
Fix corner case of wrongly applied selector as trigger (#5786)

Fixes #5766.

3 years agoDo not track processed in remove term formulas loop (#5791)
Andrew Reynolds [Wed, 20 Jan 2021 15:56:02 +0000 (09:56 -0600)]
Do not track processed in remove term formulas loop (#5791)

The assertion/tracking was spurious, since an eliminated term may occur in multiple contexts.

Fixes #5728 (which I could not reproduce currently). Adds a regression from a duplicate of that issue.

3 years agoSMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787)
Aina Niemetz [Wed, 20 Jan 2021 15:28:29 +0000 (07:28 -0800)]
SMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787)

This enables more strict handling of operators div, mod and abs
for Integer arithmetic logics.

More strict handling for '/' for Real arithmetic logics is more involved
and should be done in the parser -- instead at solving time, like is
currently done for checking that the application * is in the linear
fragment. The latter should be checked in the parser, too.
This is postponed to a later PR.

3 years agoUse arbitrary ground term assignment for sorts where isInterpretedFinite is true...
Andrew Reynolds [Wed, 20 Jan 2021 01:28:08 +0000 (19:28 -0600)]
Use arbitrary ground term assignment for sorts where isInterpretedFinite is true (#5790)

This makes a small change to our model construction to assign arbitrary values to eqc for types that are "interpreted finite", that is, have finite cardinality under the assumption that uninterpreted sorts are finite/infinite (when finite model finding is on/off). Uninterpreted sorts themselves always use the type enumerator to assign distinct values.

This fixes #5738.

This change is necessary since there was previously a mismatch between types where isFinite != isInterpretedFinite, in particular a datatype with a single constructor with a unintepreted type field as in that issue.

3 years agoImplement proofs for arith BRAB lemmas (#5784)
Alex Ozdemir [Tue, 19 Jan 2021 22:25:02 +0000 (14:25 -0800)]
Implement proofs for arith BRAB lemmas (#5784)

All changes:

Add a Pf type alias for std::shared_ptr to
expr/proof_rule.h
Add an eager proof generator to TheoryArith for preprocessing
rewrites. Right now those are proven with INT_TRUST. Will eventually
fix.
Generate proved lemmas in TheoryArithPrivate::branchIntegerVariable.
Same for TheoryArithPrivate::roundRobinBranch
Add EagerProofGenerator::mkTrustedRewrite.
Add some proofsEnabled methods.

3 years agoImplement --no-strings-lazy-pp as a preprocessing pass (#5777)
Andrew Reynolds [Fri, 15 Jan 2021 21:19:43 +0000 (15:19 -0600)]
Implement --no-strings-lazy-pp as a preprocessing pass (#5777)

This option eliminates extended functions in strings eagerly. This was incorrectly done at ppRewrite previously, which should not add lemmas. Instead, this makes this technique into a preprocessing pass. To do this, the interface for the strings preprocessor was cleaned to have fewer dependencies, and made to track a cache internally.

Fixes #5608, fixes #5745, fixes #5767, fixes #5771, fixes #5406.

3 years agoUpdates to theory preprocess equality (#5776)
Andrew Reynolds [Thu, 14 Jan 2021 13:28:55 +0000 (07:28 -0600)]
Updates to theory preprocess equality (#5776)

This makes 3 changes related to arithmetic preprocessing of equalities which revert to the original behavior of master before a129c57.

For background, the commit a129c57 unintentionally changed the default behavior slightly in 3 ways (each corrected in this PR), which led a performance regression on QF_LIA in current master.

The 3 fixes are:
(1) Rewrite equalities should be applied as a post-rewrite, not a pre-rewrite in the theory-rewrite-eq preprocessing pass. This is particularly important for equalities between ITE terms that contain other equalities recursively.
(2) theory-rewrite-eq should apply after rewriting and just before the normal theory preprocessing.
(3) The arith-brab test should call ppRewrite on the arithmetic equality it introduces, as it has a choice of whether to eliminate the equality before the lemma is sent out.