cvc5.git
8 years agoIn a ROW guard proof, if the transitivity proof does not have a disequality, we can...
guykatzz [Sat, 17 Sep 2016 00:18:56 +0000 (17:18 -0700)]
In a ROW guard proof, if the transitivity proof does not have a disequality, we can deduce that it is a constant-disequality proof and process it accordingly

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
guykatzz [Sat, 17 Sep 2016 00:10:51 +0000 (17:10 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoUse matching heuristics for EPR instantiation.
ajreynol [Sat, 17 Sep 2016 00:06:05 +0000 (19:06 -0500)]
Use matching heuristics for EPR instantiation.

8 years agoHandling a corner case where a ROW's guard is a constant disequality.
Guy [Fri, 16 Sep 2016 23:26:30 +0000 (16:26 -0700)]
Handling a corner case where a ROW's guard is a constant disequality.
If this is a simple proof (e.g., just 1 != 2), change the d_id from Transitivity to ConstantDisequality

8 years agoLet arith_proof print its own terms
Guy [Fri, 16 Sep 2016 22:43:47 +0000 (15:43 -0700)]
Let arith_proof print its own terms

8 years agoMore refactoring of cbqi, start developing new interface.
ajreynol [Fri, 16 Sep 2016 17:47:23 +0000 (12:47 -0500)]
More refactoring of cbqi, start developing new interface.

8 years agoFurther refactor cbqi.
ajreynol [Thu, 15 Sep 2016 23:44:04 +0000 (18:44 -0500)]
Further refactor cbqi.

8 years agoBegin refactoring of cbqi, remove a few dead options. Pre-skolemize by default in...
ajreynol [Thu, 15 Sep 2016 21:10:20 +0000 (16:10 -0500)]
Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by default in EPR mode.

8 years agoMake sep pto a trigger kind, track in equality engines and term database.
ajreynol [Thu, 15 Sep 2016 19:04:50 +0000 (14:04 -0500)]
Make sep pto a trigger kind, track in equality engines and term database.

8 years agoRefactor setIncomplete in quantifiers.
ajreynol [Thu, 15 Sep 2016 15:43:28 +0000 (10:43 -0500)]
Refactor setIncomplete in quantifiers.

8 years agoSupport for unique variable generation in node manager.
ajreynol [Wed, 14 Sep 2016 21:41:27 +0000 (16:41 -0500)]
Support for unique variable generation in node manager.

8 years agoLemma cache in theory sep. Minor optimization for sets. Minor improvements to EPR
ajreynol [Wed, 14 Sep 2016 15:42:39 +0000 (10:42 -0500)]
Lemma cache in theory sep. Minor optimization for sets. Minor improvements to EPR

8 years agoMinor changes to sep logic, epr, quantifier splitting.
ajreynol [Tue, 13 Sep 2016 18:36:28 +0000 (13:36 -0500)]
Minor changes to sep logic, epr, quantifier splitting.

8 years agoRefactor prenex modes.
ajreynol [Mon, 12 Sep 2016 20:48:11 +0000 (15:48 -0500)]
Refactor prenex modes.

8 years agoRemove old implementation of cbqi
ajreynol [Mon, 12 Sep 2016 19:45:38 +0000 (14:45 -0500)]
Remove old implementation of cbqi

8 years agoPrefer non-cardinality constants in term models for sep logic.
ajreynol [Mon, 12 Sep 2016 19:28:29 +0000 (14:28 -0500)]
Prefer non-cardinality constants in term models for sep logic.

8 years agoEnsure sep.nil is unique per type at NodeManager level. Add simple symmetry breaking...
ajreynol [Mon, 12 Sep 2016 18:43:02 +0000 (13:43 -0500)]
Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry breaking in theory sep.

8 years agoFix bug in unconstrained simplifier related to sep.nil/distinguished variables.
ajreynol [Fri, 9 Sep 2016 20:01:20 +0000 (15:01 -0500)]
Fix bug in unconstrained simplifier related to sep.nil/distinguished variables.

8 years agoSupport for separation logic + EPR. Refactor preprocessing of sep.nil, only allow...
ajreynol [Fri, 9 Sep 2016 19:14:09 +0000 (14:14 -0500)]
Support for separation logic + EPR. Refactor preprocessing of sep.nil, only allow sep disequal card constants when type is monotonic.  Update logics on sep regressions.

8 years agoRefactor seplog preprocess. Handle case where sep data type cannot be inferred.
ajreynol [Thu, 8 Sep 2016 20:14:19 +0000 (15:14 -0500)]
Refactor seplog preprocess. Handle case where sep data type cannot be inferred.

8 years agoMiniscope top level conjunctions for prenex normal form, allow one level miniscoping...
ajreynol [Sat, 3 Sep 2016 22:40:18 +0000 (17:40 -0500)]
Miniscope top level conjunctions for prenex normal form, allow one level miniscoping in prenex normal form.

8 years agoOption for prenex normal form
ajreynol [Sat, 3 Sep 2016 18:03:31 +0000 (13:03 -0500)]
Option for prenex normal form

8 years agoMerge pull request #91 from timothy-king/no-throw
Tim King [Fri, 2 Sep 2016 05:10:57 +0000 (22:10 -0700)]
Merge pull request #91 from timothy-king/no-throw

Relaxing the throw specifiers for the destructors for Node, TypeNode,…

8 years agoFix boolean term issue in invariants from sygus. Minor default options changes for...
ajreynol [Thu, 1 Sep 2016 21:35:06 +0000 (16:35 -0500)]
Fix boolean term issue in invariants from sygus. Minor default options changes for cbqi.

8 years agoCleanup quantifier elimination in smt engine.
ajreynol [Thu, 1 Sep 2016 15:20:48 +0000 (10:20 -0500)]
Cleanup quantifier elimination in smt engine.

8 years agoUpdates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifiers during...
ajreynol [Wed, 31 Aug 2016 22:44:42 +0000 (17:44 -0500)]
Updates to cbqi.  New strategy --cbqi-nested-qe to do qe on nested quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly.

8 years agoRelaxing the throw specifiers for the destructors for Node, TypeNode, the context...
Tim King [Thu, 1 Sep 2016 08:28:02 +0000 (01:28 -0700)]
Relaxing the throw specifiers for the destructors for Node, TypeNode, the context/ classes, and their subclasses. Fixes compilation issues with clang 3.5 and -std=c++11 'exception specification of overriding function is more lax than base version' for a couple of different classes.

8 years agoRemoving the forward declaration of QuantInfo from rewrite_engine.h.
Tim King [Thu, 1 Sep 2016 06:06:39 +0000 (23:06 -0700)]
Removing the forward declaration of QuantInfo from rewrite_engine.h.

8 years agoCleaning up the dead FORIT macros.
Tim King [Wed, 31 Aug 2016 22:59:26 +0000 (15:59 -0700)]
Cleaning up the dead FORIT macros.

8 years agoRemoving the usage of typeof from theory_sets_private.
Tim King [Wed, 31 Aug 2016 22:58:21 +0000 (15:58 -0700)]
Removing the usage of typeof from theory_sets_private.

8 years agoBeautifying theory_model.h.
Tim King [Wed, 31 Aug 2016 22:55:34 +0000 (15:55 -0700)]
Beautifying theory_model.h.

8 years agoRemoving BOOST_FOREACH from theory/sets/scrutinize.h.
Tim King [Wed, 31 Aug 2016 22:55:06 +0000 (15:55 -0700)]
Removing BOOST_FOREACH from theory/sets/scrutinize.h.

8 years agoRemoving typeof from sets normal form and beautifying the file.
Tim King [Wed, 31 Aug 2016 22:54:23 +0000 (15:54 -0700)]
Removing typeof from sets normal form and beautifying the file.

8 years agoRemoving typeof from command_executor_portfolio.cpp.
Tim King [Wed, 31 Aug 2016 22:52:41 +0000 (15:52 -0700)]
Removing typeof from command_executor_portfolio.cpp.

8 years agoRemoving typeof from didyoumean.cpp.
Tim King [Wed, 31 Aug 2016 22:35:06 +0000 (15:35 -0700)]
Removing typeof from didyoumean.cpp.

8 years agoBasic support for EPR+CBQI. Minor cleanup.
ajreynol [Fri, 26 Aug 2016 21:27:57 +0000 (16:27 -0500)]
Basic support for EPR+CBQI. Minor cleanup.

8 years agoMinor cleanup preprocessing, add ppNotifyAssertions.
ajreynol [Thu, 25 Aug 2016 20:41:27 +0000 (15:41 -0500)]
Minor cleanup preprocessing, add ppNotifyAssertions.

8 years agoOptions for counterexample guided instantiation.
ajreynol [Thu, 25 Aug 2016 18:50:45 +0000 (13:50 -0500)]
Options for counterexample guided instantiation.

8 years agoFixed two bugs
Clark Barrett [Sat, 20 Aug 2016 02:42:20 +0000 (19:42 -0700)]
Fixed two bugs

8 years agoAdded fitsSignedLong and fitsUnsignedLong
Clark Barrett [Fri, 19 Aug 2016 23:39:43 +0000 (16:39 -0700)]
Added fitsSignedLong and fitsUnsignedLong

8 years agoInitial infrastructure for ExtTheory, generalize extended term handling in TheoryStri...
ajreynol [Tue, 16 Aug 2016 17:24:58 +0000 (12:24 -0500)]
Initial infrastructure for ExtTheory, generalize extended term handling in TheoryStrings to use this.

8 years agoExpression sharing on demand in LFSC (replace definitionally equivalent child argumen...
ajreynol [Mon, 15 Aug 2016 21:30:07 +0000 (16:30 -0500)]
Expression sharing on demand in LFSC (replace definitionally equivalent child arguments after successful comparison).

8 years agoEnable bounded set membership with --fmf-bound. Map to term models for bounded set...
ajreynol [Mon, 15 Aug 2016 16:30:17 +0000 (11:30 -0500)]
Enable bounded set membership with --fmf-bound. Map to term models for bounded set membership.

8 years agoAdd a few more regressions.
ajreynol [Fri, 12 Aug 2016 17:47:54 +0000 (12:47 -0500)]
Add a few more regressions.

8 years agoMinor fixes to model construction to take singleton equivalence classes into account...
ajreynol [Fri, 12 Aug 2016 17:09:45 +0000 (12:09 -0500)]
Minor fixes to model construction to take singleton equivalence classes into account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation.

8 years agoMerge pull request #90 from 4tXJ7f/fewer_preproc_holes
guykatzz [Fri, 12 Aug 2016 14:48:43 +0000 (07:48 -0700)]
Merge pull request #90 from 4tXJ7f/fewer_preproc_holes

Add support for fewer preprocessing holes

8 years agoAdd support for fewer preprocessing holes
Andres Notzli [Wed, 10 Aug 2016 02:24:28 +0000 (19:24 -0700)]
Add support for fewer preprocessing holes

This commit adds support for the --fewer-preprocessing-holes flag. This
flag changes the preprocessing part in proofs in two ways: it (1)
removes assertions that are just restating inputs and uses the inputs
directly instead and it (2) changes the form of the preprocessed
assertions to contain the input that they originate from.

The code in this commit is mostly taken from the proofs branch in Guy's
fork.

8 years agoMinor change to strings, introduce proxy vars only when necessary.
ajreynol [Thu, 11 Aug 2016 14:03:47 +0000 (09:03 -0500)]
Minor change to strings, introduce proxy vars only when necessary.

8 years agoImprovements to strings: work on propagations for reverse normal form processing...
ajreynol [Wed, 10 Aug 2016 22:36:45 +0000 (17:36 -0500)]
Improvements to strings: work on propagations for reverse normal form processing. Better handling of disequalities, constant splitting and neg contain approximation. Introduce proxy vars for replace. Refactoring.

8 years agoMerge pull request #89 from 4tXJ7f/fix_proof_spaces
guykatzz [Tue, 9 Aug 2016 21:17:23 +0000 (14:17 -0700)]
Merge pull request #89 from 4tXJ7f/fix_proof_spaces

Fix missing/redundant spaces in proofs

8 years agoFixes for sep star rewrite.
ajreynol [Tue, 9 Aug 2016 18:11:07 +0000 (13:11 -0500)]
Fixes for sep star rewrite.

8 years agoFix missing/redundant spaces in proofs
Andres Notzli [Tue, 9 Aug 2016 03:33:24 +0000 (20:33 -0700)]
Fix missing/redundant spaces in proofs

Before, in some cases, e.g. when printing sorts and in resolution
proofs, the proofs contained redundant and/or missing spaces. With this
commit, CVC4 now prints out `(trust_f (= (Array Index Element) let10
let12)` instead of `(trust_f (= (Array Index  Element )let10 let12))`.

8 years agoMerge pull request #88 from 4tXJ7f/fix_comments
guykatzz [Sat, 6 Aug 2016 06:23:23 +0000 (23:23 -0700)]
Merge pull request #88 from 4tXJ7f/fix_comments

Minor: add/fix comments, remove redundant includes

8 years agoMinor: add/fix comments, remove redundant includes
Andres Notzli [Thu, 4 Aug 2016 22:12:54 +0000 (15:12 -0700)]
Minor: add/fix comments, remove redundant includes

8 years agoFixed an issue where arrays proofs would sometimes have an extra ")" at the end.
Guy [Wed, 3 Aug 2016 22:51:22 +0000 (15:51 -0700)]
Fixed an issue where arrays proofs would sometimes have an extra ")" at the end.

8 years agoMerge pull request #87 from 4tXJ7f/fix_oob_access
barrettcw [Wed, 3 Aug 2016 20:59:04 +0000 (13:59 -0700)]
Merge pull request #87 from 4tXJ7f/fix_oob_access

Fix out-of-bounds access in ExprManager

8 years agoPrioritize inferences when processing normal forms in strings.
ajreynol [Sat, 30 Jul 2016 14:44:42 +0000 (09:44 -0500)]
Prioritize inferences when processing normal forms in strings.

8 years agoThe "aggressive" optimizer for lemma L now returns the conjunction of all lemmas...
Guy [Thu, 28 Jul 2016 20:40:36 +0000 (13:40 -0700)]
The "aggressive" optimizer for lemma L now returns the conjunction of all lemmas L' that originated from L and were used in the unsat core

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Thu, 28 Jul 2016 18:24:59 +0000 (11:24 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoBug fix involving negated lemmas
Guy [Thu, 28 Jul 2016 18:24:07 +0000 (11:24 -0700)]
Bug fix involving negated lemmas

8 years agoFix bug 749.
ajreynol [Thu, 28 Jul 2016 16:21:59 +0000 (11:21 -0500)]
Fix bug 749.

8 years agoAdd the negative conjunction case
Guy [Thu, 28 Jul 2016 16:01:52 +0000 (09:01 -0700)]
Add the negative conjunction case

8 years agoFix out-of-bounds access in ExprManager
Andres Notzli [Wed, 27 Jul 2016 21:06:56 +0000 (14:06 -0700)]
Fix out-of-bounds access in ExprManager

The size of `d_exprStatisticsVars` was `LAST_TYPE` which was not enough
because the INC_STAT macro tries to access
`d_exprStatisticsVars[LAST_TYPE]` in some cases, resulting in an
out-of-bounds access. Found bug with UBSan.

8 years agoProper instrumentation of the preprocessing phase
Guy [Thu, 28 Jul 2016 02:03:13 +0000 (19:03 -0700)]
Proper instrumentation of the preprocessing phase

8 years agoproper handling of ITEs
Guy [Thu, 28 Jul 2016 01:17:41 +0000 (18:17 -0700)]
proper handling of ITEs

8 years agoProper handling of IFF lemmas in the unsat core.
Guy [Wed, 27 Jul 2016 21:27:05 +0000 (14:27 -0700)]
Proper handling of IFF lemmas in the unsat core.
Don't return duplicates in the unsat core

8 years agoAdded an option for a more aggressive weakest implicant optimization
Guy [Wed, 27 Jul 2016 19:54:29 +0000 (12:54 -0700)]
Added an option for a more aggressive weakest implicant optimization

8 years agoIf we can't find a weaker implicant, fail gracefully and return the original lemma
Guy [Wed, 27 Jul 2016 16:46:24 +0000 (09:46 -0700)]
If we can't find a weaker implicant, fail gracefully and return the original lemma

8 years agoMerge pull request #86 from 4tXJ7f/fix_warnings
guykatzz [Wed, 27 Jul 2016 05:07:35 +0000 (22:07 -0700)]
Merge pull request #86 from 4tXJ7f/fix_warnings

Fix warnings in src/proof

8 years agoFix warnings in src/proof
Andres Notzli [Wed, 27 Jul 2016 04:07:24 +0000 (21:07 -0700)]
Fix warnings in src/proof

Fix warning due to `ProofLetCount` being defined as `struct` in
`proof_utils.h` and `class` in `proof.h`. Fix warnings due to different
number of arguments of `printConstantDisequalityProof()` and
`printTheoryLemmaProof()` in subclasses.

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Tue, 26 Jul 2016 23:38:06 +0000 (16:38 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoBug fix:
Guy [Tue, 26 Jul 2016 23:37:57 +0000 (16:37 -0700)]
Bug fix:
If a lemma (a disjunction) has a "false" literal in it, it can be ignored, but a "true" literal really should stay

8 years agoAdd option to minimize sygus solutions based on using weakest implicants of instantia...
ajreynol [Tue, 26 Jul 2016 22:55:09 +0000 (17:55 -0500)]
Add option to minimize sygus solutions based on using weakest implicants of instantiations in unsat cores.

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Tue, 26 Jul 2016 22:03:37 +0000 (15:03 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoLetification of BV constants
Guy [Tue, 26 Jul 2016 22:03:27 +0000 (15:03 -0700)]
Letification of BV constants

8 years agoMinor improvements to strings related to constant splitting, including a few options...
ajreynol [Tue, 26 Jul 2016 20:15:46 +0000 (15:15 -0500)]
Minor improvements to strings related to constant splitting, including a few options (disabled by default).

8 years agoAdded functionality to retrieve a lemma's "weakest implicant" in the unsat core....
Guy [Tue, 26 Jul 2016 20:09:31 +0000 (13:09 -0700)]
Added functionality to retrieve a lemma's "weakest implicant" in the unsat core. Currently, lemmas that are not conjunctions and their own weakest implicants; but for lemmas that *are* conjunctions, we may return only a subset of the conjuncts.

8 years agoBug fix
Guy [Tue, 26 Jul 2016 00:24:39 +0000 (17:24 -0700)]
Bug fix

8 years agoPropagate the usage of proof let maps into constant disequality proofs
Guy [Tue, 26 Jul 2016 00:20:14 +0000 (17:20 -0700)]
Propagate the usage of proof let maps into constant disequality proofs

8 years agoBug fix
Guy [Mon, 25 Jul 2016 23:52:27 +0000 (16:52 -0700)]
Bug fix

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Mon, 25 Jul 2016 22:59:49 +0000 (15:59 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agocleanup
Guy [Mon, 25 Jul 2016 06:24:40 +0000 (23:24 -0700)]
cleanup

8 years agoUse letification for the aliasing declarations as well (consequently, print the globa...
Guy [Mon, 25 Jul 2016 05:35:05 +0000 (22:35 -0700)]
Use letification for the aliasing declarations as well (consequently, print the global let map before the aliasing part)

8 years agoProper handling for lemmas that are conjuncts:
Guy [Mon, 25 Jul 2016 03:56:08 +0000 (20:56 -0700)]
Proper handling for lemmas that are conjuncts:
Record a separate recipe for each conjunct, but have as the "original lemma" in this recipe the complete conjunction, so that we can report this to the theory solver later, if asked.

Refactoring: instead of propagating the proof recipes from the theory engine to the prop engine and cnf stream to be registered there, just register them at the theory engine - as the prop engine and cnf stream don't change them.

8 years agoMinor, error handling for polymorphism + sep logic.
ajreynol [Fri, 22 Jul 2016 15:59:16 +0000 (10:59 -0500)]
Minor, error handling for polymorphism + sep logic.

8 years agoFixes for strings, explanations for constant split propagations, substr under concat...
ajreynol [Thu, 21 Jul 2016 15:56:09 +0000 (10:56 -0500)]
Fixes for strings, explanations for constant split propagations, substr under concat rewrite. Avoid duplicate re.range length lemmas.

8 years agoInfrastructure for storing and printing heap models for separation logic. Ensure...
ajreynol [Wed, 20 Jul 2016 18:28:01 +0000 (13:28 -0500)]
Infrastructure for storing and printing heap models for separation logic. Ensure value of sep.nil is correct in models. Print instantiations as sexprs.

8 years agoPrint only instantiations that are in the unsat core when --proof is enabled. Add...
ajreynol [Wed, 20 Jul 2016 16:52:37 +0000 (11:52 -0500)]
Print only instantiations that are in the unsat core when --proof is enabled.  Add option to minimize sygus solutions based on unsat core (disabled by default).

8 years agoInfer conflicts in strings based on abstracting equality as contains. Minor cleanup.
ajreynol [Wed, 20 Jul 2016 16:08:11 +0000 (11:08 -0500)]
Infer conflicts in strings based on abstracting equality as contains. Minor cleanup.

8 years agoBug fix
Guy [Wed, 20 Jul 2016 02:33:15 +0000 (19:33 -0700)]
Bug fix

8 years agoAllow a caller to query whether an unsat core is available or not
Guy [Wed, 20 Jul 2016 02:13:01 +0000 (19:13 -0700)]
Allow a caller to query whether an unsat core is available or not

8 years agoAdd infrastructure for tracking instantiation lemmas (for proofs, and minimization...
ajreynol [Tue, 19 Jul 2016 15:32:37 +0000 (10:32 -0500)]
Add infrastructure for tracking instantiation lemmas (for proofs, and minimization of --dump-instantiations, qe and synthesis solutions). Eliminate quantified arithmetic variables that only have lower/upper bounds. Cleanup strings preprocess, minor fix for str.replace semantics. Reorder cegqi before fmf. Minor cleanup.

8 years agoRefactor strings extf evaluation info. Ensure strings eager preprocess eliminates...
ajreynol [Sat, 16 Jul 2016 14:03:11 +0000 (09:03 -0500)]
Refactor strings extf evaluation info. Ensure strings eager preprocess eliminates all extf symbols during ppRewrite. Add options stringGuessModel and stringUfReduct. Minor optimizations.

8 years agoMoved the assertion to a better spot
Guy [Fri, 15 Jul 2016 23:53:54 +0000 (16:53 -0700)]
Moved the assertion to a better spot

8 years agoThe ProofManager now allows theory solvers to get their lemmas that participate in...
Guy [Fri, 15 Jul 2016 23:48:25 +0000 (16:48 -0700)]
The ProofManager now allows theory solvers to get their lemmas that participate in the unsat cores.
Currently this is only limited to lemmas generated via the d_out->lemma() interface, i.e. no propagations
and conflict lemmas.

8 years agoMinor simplification to normal form explanations.
ajreynol [Fri, 15 Jul 2016 14:39:09 +0000 (09:39 -0500)]
Minor simplification to normal form explanations.

8 years agoMinor fix to last commit.
ajreynol [Fri, 8 Jul 2016 11:49:24 +0000 (06:49 -0500)]
Minor fix to last commit.

8 years agoSimplifications for strings normal forms, fix case for concat reps in normal forms.
ajreynol [Fri, 8 Jul 2016 02:03:25 +0000 (21:03 -0500)]
Simplifications for strings normal forms, fix case for concat reps in normal forms.

8 years agoEnsure heap disjointness in sep refinements.
ajreynol [Thu, 7 Jul 2016 22:14:56 +0000 (17:14 -0500)]
Ensure heap disjointness in sep refinements.

8 years agoRefactoring of strings preprocess module. When enabled, apply eager preprocess during...
ajreynol [Thu, 7 Jul 2016 20:22:40 +0000 (15:22 -0500)]
Refactoring of strings preprocess module. When enabled, apply eager preprocess during ppRewrite instead of during processAssertions. Simplify reduction for contains.  Fix bug in explanations for F_EndpointEq. Minor cleanup for sep.