Andrew Reynolds [Fri, 29 Sep 2017 19:28:52 +0000 (14:28 -0500)]
Simplify representation of inversion Skolems for bv cegqi (#1164)
* Simplify intermediate representation of inversion skolems for cegqi bit-vectors. Cache bv inversion status globally in QuantifierEngine. Generalize virtual term policy for marking eligible instantiation terms. Enable regression.
* Enable other regression
Andrew Reynolds [Fri, 29 Sep 2017 12:23:22 +0000 (07:23 -0500)]
Initial working version of BV word-level instantiation (#1158)
* Initial work on BV CEGQI, still working on avoid circular dependencies with inversion skolems.
* Guard by option, minor notes.
* Minor
* Minor fixes.
* Minor
Andres Noetzli [Fri, 29 Sep 2017 08:14:51 +0000 (01:14 -0700)]
Better hash function for pairs (#1157)
CVC4 was computing hashes for pairs of objects by simply XORing the
hashes of the two objects. This commit implements a better way of
combining hashes based on the FNV-1a hash algorithm. The algorithm is
public domain.
Andrew Reynolds [Fri, 29 Sep 2017 04:58:03 +0000 (23:58 -0500)]
Update symbol table to support operator overloading (#1154)
Mathias Preiner [Fri, 29 Sep 2017 03:32:36 +0000 (20:32 -0700)]
Fix output of --show-config for readline. (#1159)
cvc4 --show-config reported the wrong configuration for readline since
HAVE_LIBREADLINE is set to 0 or 1 but was checked with #ifdef.
Andrew Reynolds [Thu, 28 Sep 2017 21:31:02 +0000 (16:31 -0500)]
Cegqi refactor prep bv (#1155)
* Preparing for bv instantiation, initial working version.
* Undoing bv changes to break up into smaller commit.
Andrew Reynolds [Thu, 28 Sep 2017 12:23:33 +0000 (07:23 -0500)]
Improve finite model finding for recursive predicates (#1150)
* Optimization for model finding for recursive functions involving branching positions. Update documentation, add regressions.
* Simplifications, update comments.
Andrew Reynolds [Wed, 27 Sep 2017 23:49:41 +0000 (18:49 -0500)]
Minor fixes for partial quantifier elimination. (#1147)
This forces "counterexample lemmas" (the formula B => ~phi[e] on page 23 of http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf) to be added during TheoryQuantifiers::preRegisterTerm instead of at full effort check. This is required to ensure that CVC4's partial quantifier elimination algorithm produces correct results.
Some background:
"get-qe" and "get-qe-disjunct" are commands in the SMT2 parser. Here is how they can be used:
[declarations]
[assertions A]
(get-qe (exists X F))
returns a ground formula F' such that A ^ F' and A ^ (exists X F) are equivalent.
The command "get-qe-disjunct" provides an interface for doing an incremental version of "get-qe".
[declarations]
[assertions A]
(get-qe-disjunct (exists X F))
returns a ground formula F1' such that A ^ F' implies A ^ (exists X F). It moreover has the property that if you call:
[declarations]
[assertions A]
(assert F1')
(get-qe-disjunct (exists X F))
this will give you a formula F2' where eventually:
[declarations]
[assertions A]
(assert (not (or F1' ... Fn')))
(get-qe-disjunct (exists X F))
will either return "true" or "false", for some finite n.
Here is an example that failed before this commit:
(set-logic LIA)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(assert (or (not (>= (+ a (* (- 1) b)) 1)) (not (>= (+ c (* (- 1) d)) 0))))
(get-qe-disjunct (exists ((x Int)) (and (> a b) (> c x) (> d x))))
This should return:
(not (or (not (>= (+ a (* (- 1) b)) 1)) (>= (+ c (* (- 1) d)) 1)))
Previously it was returning:
false
This is because the cbqi algorithm needs to assume the negation of the quantified formula we are doing qe on before it makes any decision.
The get-qe-partial feature is being requested by Cesare and Daniel Larraz for Kind2.
This improves our performance on quantified LIA/LRA:
https://www.starexec.org/starexec/secure/details/job.jsp?id=24480
see CVC4-092617-2-fixQePartial
Aina Niemetz [Wed, 27 Sep 2017 20:45:27 +0000 (13:45 -0700)]
CEGQI for BV: Add inverse for BITVECTOR_MULT. (#1153)
This implements side conditions and the instantiation via word-level inversion for operator BITVECTOR_MULT.
Andrew Reynolds [Wed, 27 Sep 2017 11:50:47 +0000 (06:50 -0500)]
Add quantifiers API example, fixes #879 (#1146)
Andres Noetzli [Wed, 27 Sep 2017 07:43:30 +0000 (00:43 -0700)]
Fix seeking for buffered input (#1145)
CVC4's implementation of seek was calculating the pointer difference
between the current position in the input and the seek point to
determine how many characters to consume. This was causing problems when
ANTLR was seeking to a pointer on a line after the current line because
it would result in a big number of characters to consume because each
line is allocated separately. This resulted in issue #1113, where CVC4
was computing a large number of characters to consume and would block
until it received all of them. This commit fixes and simplifies the
code by simply consuming characters until the seek point is reached
without computing a count beforehand.
Martin Brain [Wed, 27 Sep 2017 03:00:17 +0000 (20:00 -0700)]
Fix type checking of to_real (#1127)
to_real takes a single argument as given in kinds.
Martin Brain [Wed, 27 Sep 2017 00:21:51 +0000 (17:21 -0700)]
Improve FP rewriter: const folding, other (#1126)
Tim King [Tue, 26 Sep 2017 20:02:32 +0000 (13:02 -0700)]
Fixing CIDs
1172014 and
1172013: Initializing members of GetProofCommand and GetModelCommand to nullptr. (#1142)
Tim King [Tue, 26 Sep 2017 18:26:40 +0000 (11:26 -0700)]
Fixing Cid
1172009 (#1141)
Tim King [Tue, 26 Sep 2017 16:36:52 +0000 (09:36 -0700)]
Fixing CID
1172020: Initializing CDHashMap::iterator::d_it to nullptr. (#1139)
Tim King [Tue, 26 Sep 2017 14:33:31 +0000 (07:33 -0700)]
Fixing CID
1362903: Initializing d_bvp to nullptr. (#1136)
Tim King [Tue, 26 Sep 2017 09:28:57 +0000 (02:28 -0700)]
CID
1362904: Initializing GetInstantiationsCommand::d_smtEngine to nullptr. (#1135)
Andres Noetzli [Tue, 26 Sep 2017 07:46:14 +0000 (00:46 -0700)]
Fix build for old GMP version (#1114)
Older versions of GMP in combination with newer versions of GCC and
C++11 cause errors [0]. This commit adds the necessary includes of
<cstddef>.
[0] https://gcc.gnu.org/gcc-4.9/porting_to.html
Tim King [Tue, 26 Sep 2017 06:51:42 +0000 (23:51 -0700)]
Fixing CIDs
1172012 and
1172011: Initiallzing d_exprManager to nullptr in const_iterator. (#1140)
Andrew Reynolds [Tue, 26 Sep 2017 00:43:27 +0000 (19:43 -0500)]
Cegqi refactor substitutions (#1129)
This refactors the apply substitution mechanism for counterexample-guided quantifier instantiation (CEGQI).
Improvements to the code:
(1) Methods have been added to the TermProperties class that summarize their theory-independent behavior (including "getModifiedTerm", "isBasic" etc.). For now, I have not made a "TermPropertiesArith" class yet since this will require more fundamental refactoring.
(2) The terminology "has_coeff" is replaced "is_non_basic" throughout.
(3) Added the applySubstitutionToLiteral method.
(4) Both applySubstitution and applySubstitutionToLiteral are now private within CegInstantiator. This means that theory-specific instantiators do not need to implement custom ways of applying substitutions (previously the arithmetic instantiator was).
(5) applySubstitutionToLiteral is automatically called on all literals (see line 297 of ceg_instantiator.cpp). This means that BvInstantiator::processAssertion is now called on substituted literals. So for instance if our context contains two literals:
x = bv2, bvmul(x,y) = bv4
Say we are asked to solve for x first, and return the substitution {x -> bv2}, then if we are later asked to solve for y, we will call processAssertion for the literal bvmul(bv2,y)=bv4
(6) LIA-specific information "d_theta" in SolvedForm is encapsulated inside the class (with the understanding that this will be made virtual).
This commit has no impact on quantified LIA / LRA: https://www.starexec.org/starexec/secure/details/job.jsp?id=24480
(see CVC4-092217-cegqiRefactorSubs)
Tim King [Mon, 25 Sep 2017 23:06:14 +0000 (16:06 -0700)]
Initializing BVMinisat Solver::notify to nullptr. (#1132)
Andrew Reynolds [Mon, 25 Sep 2017 21:42:02 +0000 (16:42 -0500)]
Fix bug related to sort inference + subtypes. (#1125)
Tim King [Mon, 25 Sep 2017 20:02:48 +0000 (13:02 -0700)]
Fixing CID
1362917: There was a branch where d_issup was not initialized. Switching members of InstantiationEngine to uniqur_ptr to simplify such cases. (#1133)
Tim King [Mon, 25 Sep 2017 15:58:45 +0000 (08:58 -0700)]
Fixing CID
1362895: Initializing d_bvp to nullptr. (#1137)
* Fixing CID
1362895: Initializing d_bvp to nullptr. Miscellaneous cleanup.
Tim King [Mon, 25 Sep 2017 06:20:12 +0000 (23:20 -0700)]
CID
1362907: Initializing d_smtEngine to nullptr. (#1134)
Andrew Reynolds [Thu, 21 Sep 2017 08:20:09 +0000 (03:20 -0500)]
Sygus inv templ refactor (#1110)
* Decouple single invocation techniques from deep embedding techniques. Embed templates for invariant synthesis into grammar instead of as a global substitution. Add regression.
* Update comment on class
* Cleanup
* Comments for sygus type construction.
Andrew Reynolds [Thu, 21 Sep 2017 00:32:46 +0000 (19:32 -0500)]
Extend quantifier-free UF solver to higher-order. This includes an ex… (#1100)
* Extend quantifier-free UF solver to higher-order. This includes an extensionality inference, and lazy conversion from APPLY_UF to HO_APPLY terms.Implements collectModelInfo and theory combination for HO_APPLY terms.
* Update comments, minor changes to functions. Update APPLY_UF skolem to be user-context dependent.
* Remove unused NodeList
Andres Noetzli [Wed, 20 Sep 2017 18:24:13 +0000 (11:24 -0700)]
Fix issue #1081, memory leak in cmd executor (#1109)
The variable `g` could be set multiple times depending on
the options (e.g. a combination of `--dump-unsat-cores`
and `--dump-synth`), which could lead to memory leaks and
missing output. This commit fixes the issue by replacing
`g` with a list of `getterCommands` that are all executed and
deleted.
Martin [Wed, 20 Sep 2017 01:30:24 +0000 (02:30 +0100)]
Add FP type enumerator and cardinality computer (#1104)
Tim King [Tue, 19 Sep 2017 22:51:50 +0000 (15:51 -0700)]
Fixing a null pointer dereference in the cvc3 compatibility layer. (#1089)
Tim King [Tue, 19 Sep 2017 20:17:04 +0000 (13:17 -0700)]
Removing a potentially invalid comparison in the TPTP parser. (#1091)
Andres Noetzli [Tue, 19 Sep 2017 16:43:58 +0000 (09:43 -0700)]
Fix issue #1074, improve non-fatal error handling (#1075)
Commit
54d24c786d6a843cc72dfb5e377603349ea5e420 was
changing CVC4 to handle certain non-fatal errors
(such as calling get-unsat-core without a proceding
unsat check-sat command) without terminating the
solver. In the case of get-unsat-cores, the changes
lead to the solver crashing because it was trying to
print an unsat core initialized with the default
constructor, so the member variable d_smt was NULL,
which lead to a dereference of a null pointer.
One of the issues of the way non-fatal errors were
handled was that the error reporting was done in the
invoke() method of the command instead of the
printResult() method, which lead to the error
described above and other issues such as a call to
get-value printing a value after reporting an error.
This commit aims to improve the design by adding a
RecoverableModalException for errors that the solver
can recover from and CommandRecoverableFailure to
communicate that a command failed in a way that does
not prohibit the solver from continuing to execute.
The exception RecoverableModalException is thrown by
the SMTEngine and the commands catch it and turn it
into a CommandRecoverableFailure. The commit changes
all error conditions from the commit above and adds a
regression test for them.
Andrew Reynolds [Tue, 19 Sep 2017 11:31:22 +0000 (06:31 -0500)]
Refactor cegqi instantiation infrastructure so that it is more independent of instantiation for LIA. (#1111)
Andrew Reynolds [Tue, 19 Sep 2017 06:03:56 +0000 (01:03 -0500)]
Fix issue #1105 involving string to int (#1112)
This was introduced by changing the implementation of "isNumber" in this commit:
a94318b
This fixes issue #1105.
Martin [Tue, 19 Sep 2017 00:14:05 +0000 (01:14 +0100)]
Floating point symfpu support (#1103)
- Update the parser to the new constant construction
- Fix the problem with parsing +/-zero and remove some dead code
- Extend the interface for literal floating-point values.
- Add a constructor so that a parameteric operator structure can be created from a type
- Add constructors so parametric operator constants can be easily converted
- Update SMT2 printing so that it uses the informative output
Tim King [Mon, 18 Sep 2017 06:40:17 +0000 (23:40 -0700)]
Moving the CVC4_PUBLIC attribute to the beginning of operator++. (#1107)
Removes the following warning when compiling with gcc version 4.8.4 :
../../../../../src/expr/kind_template.h:95:55: warning: '__visibility__' attribute ignored on non-class types [-Wattributes]
Tested with clang-3.5.
Martin [Fri, 15 Sep 2017 03:04:20 +0000 (04:04 +0100)]
Make floating-point comparison operators chainable (#1101)
Floating-point comparison operators are chainable according to the standard.
makaimann [Fri, 15 Sep 2017 00:50:16 +0000 (17:50 -0700)]
Add missing CVC4_PUBLIC in kind_template (#1078)
Andres Noetzli [Thu, 14 Sep 2017 22:14:09 +0000 (15:14 -0700)]
Enable ccache compression, increase cache size (#1099)
This commit enables compression for ccache, increases the cache size to 1GB and
resets the ccache statistics before each run.
Andrew Reynolds [Thu, 14 Sep 2017 19:12:22 +0000 (14:12 -0500)]
Remove unhandled subtypes (#1098)
* Remove unhandled subtypes, which consequently makes typing rules uniformly stricter based on weakening the subtype relation. Ensure coercions in the smt2 and cvc parser for Real decimal constants whose type is Integer. Ensure type annotations are computed during preRewrite to ensure rewriting (which does not preserve types) does not impact term construction for parametric datatypes. This fixes issue #1048 (we now give an type exception).
* Update unit test for parametric datatypes to reflect new subtyping relation.
* Remove deprecated test.
* Make array construction for lambdas work with new subtype relations to handle lambdas like (lambda ((x Int) (y Int)) (ite (= x 0) 0.5 0.0)).
Tim King [Thu, 14 Sep 2017 17:09:40 +0000 (10:09 -0700)]
Simplifying the throw specifier of SmtEngine::checkSat and related calls to CVC4::Exception. (#1085)
Martin [Thu, 14 Sep 2017 03:51:50 +0000 (04:51 +0100)]
Floating point symfpu support (#1093)
Changes needed for the bit-blasting floating-point solver which are outside of it's area and / or applicable independently.
Andrew Reynolds [Thu, 14 Sep 2017 02:08:28 +0000 (21:08 -0500)]
Add new kinds required for higher-order. (#1083)
This consists of a binary apply symbol HO_APPLY that returns the result of applying its first argument to its second argument. Update the UF rewriter to ensure that non-standard APPLY_UF applications are rewritten into curried applications of HO_APPLY.
Andrew Reynolds [Thu, 14 Sep 2017 00:26:35 +0000 (19:26 -0500)]
Add isConst check for lambda expressions. (#1084)
Add isConst check for lambda expressions by conversions to and from an Array representation where isConst is implemented. This enables check-model to succeed on higher-order benchmarks. Change the builtin rewriter for lambda to attempt to put lambdas into constant form. Update regression.
Andres Noetzli [Wed, 13 Sep 2017 21:13:35 +0000 (14:13 -0700)]
Make ccache work with Clang on Travis (#1097)
This commit uses a workaround [0] to get ccache to work
with Clang on Travis.
[0] https://github.com/travis-ci/travis-ci/issues/5383#issuecomment-
224630584
Andrew Reynolds [Wed, 13 Sep 2017 21:08:01 +0000 (16:08 -0500)]
Modify equality engine to allow operators to be marked as external terms (#1082)
This is required for reasoning higher-order, since we may have equalities between functions, which are operators of APPLY_UF terms.
This commit gets around the previous 1% slowdown by modifying the changes to the equality engine to be minimal impact. Previously the "isInternal" flag could be reset to false after a term is marked as internal=true. This provides an interface for whether operators of a kind should be marked as internal=false from the start. When using higher-order, APPLY_UF operators will be marked as being external when the higher-order option ufHo is set to true.
This has <.001% impact on performance on QF smtlib : https://www.starexec.org/starexec/secure/details/job.jsp?id=24445
Andres Noetzli [Wed, 13 Sep 2017 08:31:30 +0000 (01:31 -0700)]
Remove unused RecordSelect and TupleSelect (#1087)
Commit
62b673a6b8444c14c169a984dd6e3fc8f685851e remove most of the
record/tuple infrastructure but did not remove the classes RecordSelect and
TupleSelect which lead to issues with Java bindings (the references to the
corresponding mkConst implementations could not be resolved). This commit
removes the remaining traces of those classes.
Andres Noetzli [Wed, 13 Sep 2017 03:52:10 +0000 (20:52 -0700)]
Enable ccache on Travis, disable debug symbols (#1094)
Enable ccache on Travis for faster compile times. Also
disable debug symbols for the debug builds on Travis to
use the available cache more efficiently. Note: this
change only works on GCC, support for Clang will require
additional changes but the time savings should already be
pretty significant.
Andrew Reynolds [Tue, 12 Sep 2017 23:48:27 +0000 (18:48 -0500)]
Initial infrastructure for BV instantiation via word-level inversions. (#1056)
* Initial infrastructure for BV instantiation via word-level inversions.
* Minor clean up.
* Change visited to unordered set.
Tim King [Tue, 12 Sep 2017 00:07:16 +0000 (17:07 -0700)]
Adding reasonable breaks in switch statement in TheoryStrings::normalizeRegexp. Minor code reorganization and applying clang-tidy to the function. (#1079)
Tim King [Mon, 11 Sep 2017 15:55:56 +0000 (08:55 -0700)]
Addressing a coverity scan complaint in theory_strings.cpp. I believe the root cause is that d_normal_forms_exp[r[0]] could have referred to different vectors (as operator[] is inserting for maps). (#1080)
Andrew Reynolds [Sun, 10 Sep 2017 06:12:34 +0000 (08:12 +0200)]
Ensure that expand definitions is called on all non-variable expressi… (#1070)
* Ensure that expand definitions is called on all non-variable expressions. In particular, it is necessary that the sets theory is notified when a set universe term occurs in the input to ensure options are set correctly. The commit moves this check from within check() to expandDefinitions(), and also adds the check for join image which relies on universe set. This fixes a bug reported by Arjun. Add and update regressions.
* Add comments concerning expandDefinitions
* Expand comment, move to .h
Andrew Reynolds [Thu, 7 Sep 2017 09:50:59 +0000 (11:50 +0200)]
Properly handle user cardinality constraints for uf-ss=none. (#1068)
Mathias Preiner [Tue, 5 Sep 2017 22:58:59 +0000 (15:58 -0700)]
Fix link in configure.ac.
Andrew Reynolds [Tue, 5 Sep 2017 05:57:40 +0000 (07:57 +0200)]
Remove support for conversions between uint32/uint16 and string. (#1069)
* Remove support for conversions between uint32/uint16 and string.
* Temporarily disable regression.
Aina Niemetz [Fri, 1 Sep 2017 16:57:28 +0000 (09:57 -0700)]
Add travis debug build with cln. (#1066)
Until now, all travis builds where built with gmp. This commit adds an additional debug build built with cln.
Andres Noetzli [Fri, 1 Sep 2017 05:25:27 +0000 (22:25 -0700)]
Add GCC7 jobs to Travis (#1054)
This commit adds two jobs (debug, with portfolio, test groups 0 and 1) to Travis.
Both jobs are added using matrix.include, based on the example in the documentation:
https://docs.travis-ci.com/user/languages/cpp/#GCC-on-Linux . This
unfortunately requires some code duplication but there does not seem to be a
way to do it in a much better fashion.
Andres Noetzli [Fri, 1 Sep 2017 00:39:16 +0000 (17:39 -0700)]
Replace CVC4_THREADLOCAL in interactive_shell (#1065)
Commit
546d795470ca7c30fc62fe9b6c7b8e5838e1eed4
caused our nightly builds to fail because it did
not replace CVC4_THREADLOCAL with
CVC4_THREAD_LOCAL in interactive_shell. This
commit fixes the issue and adds readline to
Travis, s.t. readline related code gets compiled
as part of our CI tests.
Andrew Reynolds [Thu, 31 Aug 2017 12:26:26 +0000 (14:26 +0200)]
Answer unknown when uf-ss=no-minimal is combined with cardinality constraints from user input, add regressions. (#1060)
Andres Noetzli [Thu, 31 Aug 2017 03:55:27 +0000 (20:55 -0700)]
Use thread_local instead of compiler extensions (#210)
C++11 introduced the thread_local keyword, so we don't need to use
non-standard extensions or our custom pthread extension anymore.
The behavior was previously introduced as a workaround in commit
753a072c542c1c254d7c6adbf10e091ba585ede5. This commit
introduces the macro CVC4_THREAD_LOCAL that can be used to
declare variables as thread local. For Swig, this macro is defined to
be empty.
Andrew Reynolds [Wed, 30 Aug 2017 22:59:24 +0000 (00:59 +0200)]
Fix model construction for parametric types (#1059)
Fix model construction for parametric types so that we enumerate types in order of dependencies, and avoid subterms of previously enumerated values.
There was a bug in model construction for parametric types which was related to enumerating values that are subterms of other previously enumerated values created during model construction (which were not recorded).
This commit adds all subterms of values we enumerate to the "already used value" sets of their respective types, as reflected in the changes to TypeSet.
There is an extra wrinkle in making the above change, which was caught by the regression test/regress/regress0/fmf/dt-proper-model.smt2. The issue is specific to finite model finding and can be corrected by ensuring that base types (e.g. uninterpreted sorts) are enumerated first.
The change to TheoryModel::buildModel that replaces "allTypes" with "type_list" fixes this wrinkle. This constructs a partially ordered list of types where T1 comes before T2 if values of T2 can contain terms of type T1 but not vice versa. Ordering our enumeration in this way is probably a good idea in general. This ensures we enumerate values for equivalence classes of e.g. Int before (Array Int Int) and means we exclude fewer intermediate values during model construction.
Mathias Preiner [Wed, 30 Aug 2017 16:04:36 +0000 (09:04 -0700)]
Remove Coverity SSL certificate workaround from Travis configuration. (#1058)
Coverity works without the SSL certificate workaround and is not needed anymore. Note that we don't require sudo anymore and we could switch to container-based Travis builds (instead of VM-based). However, container-based environments only provide 4G of memory (instead of 7.5G for VMs) , which is not enough for the current CVC4 build environment.
Mathias Preiner [Tue, 29 Aug 2017 23:10:30 +0000 (16:10 -0700)]
Fix indentation for disabled Java tests.
Mathias Preiner [Tue, 29 Aug 2017 23:03:31 +0000 (16:03 -0700)]
Disable Java tests for now until they get fixed.
Pat Hawks [Mon, 28 Aug 2017 21:13:22 +0000 (16:13 -0500)]
Run Ant on Travis
Andres Noetzli [Mon, 28 Aug 2017 17:22:31 +0000 (10:22 -0700)]
Travis: Package instead of download for cxxtest (#1055)
Before this commit, we were downloading cxxtest from Sourceforge. This commit
instead installs the Ubuntu package, which is easier and more reliable. Instead
of adding the package to the list of packages for Coverity and the common list
of packages, this commit changes the Coverity package list to just refer to the
common list of packages.
Aina Niemetz [Fri, 25 Aug 2017 22:39:16 +0000 (15:39 -0700)]
Move LFSC checker out of the CVC repository. (#222)
LFSC now lives outside of the CVC4 repository and is not part of the CVC4 distribution
anymore. As a consequence, we
+ Add --with-lfsc and --with-lfsc-directory as configure options.
In the case where CVC4 has not been built with integrated LFSC, all code that interacts with
LFSC is disabled.
+ Disable proof checking if CVC4_USE_LFSC is not defined.
Configuring the build with --check-proofs but without --with-lfsc results in an error.
+ Do not call LFSC's cleanup function (but we should in the future).
LFSC checker segfaults during cleanup on regression testcase regress0/bv/core/bitvec7.smt.
Disabled call to lfscc_cleanup until the problem in lfscc is fixed.
+ Disable building with LFSC for the distcheck travis build since it is not part of the distribution
anymore. Further, make distcheck with LFSC would require to call contrib/get-lfsc-checker
before calling make check on the temp build (the build of the unpacked distribution tar ball).
Aina Niemetz [Fri, 25 Aug 2017 20:29:04 +0000 (13:29 -0700)]
Added missing includes (algorithm).
Algorithm was previously removed from src/util/regexp.h which broke
compilation on some platforms.
Pat Hawks [Thu, 24 Aug 2017 22:31:09 +0000 (17:31 -0500)]
Test Java API on CI
Andres Noetzli [Thu, 24 Aug 2017 17:08:39 +0000 (10:08 -0700)]
Add include to fix build
Andrew Reynolds [Thu, 24 Aug 2017 12:09:43 +0000 (14:09 +0200)]
Merge pull request #191 from timothy-king/cleanup-regexp
Cleaning up the CVC4::String class.
Andres Noetzli [Wed, 23 Aug 2017 18:13:07 +0000 (11:13 -0700)]
Fix typos
Tim King [Wed, 23 Aug 2017 22:49:32 +0000 (15:49 -0700)]
Removing TODO for 'Optimize via the iterator'. Not a priority. (#1051)
Aina Niemetz [Tue, 22 Aug 2017 01:33:29 +0000 (18:33 -0700)]
Cleanup: use Assert rather than C assert. (#1052)
Clark Barrett [Tue, 22 Aug 2017 00:30:45 +0000 (17:30 -0700)]
Updated NYU -> Stanford
Mathias Preiner [Mon, 21 Aug 2017 17:06:02 +0000 (10:06 -0700)]
Change Bugzilla urls to Github issues.
Andres Noetzli [Thu, 17 Aug 2017 15:51:51 +0000 (08:51 -0700)]
Remove unused SubrangeBound(s) classes (#221)
As discussed in pull request #220, commit
360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 mostly got rid of SubrangeBound(s).
There were still a few mentions of it left in the code, most of them commented
out. The occurrences in expr.i and expr_manager.i, however, created issues with
the Python wrapper. This commit removes the SubrangeBound(s) implementation and
other leftovers.
ajreynol [Thu, 17 Aug 2017 09:53:11 +0000 (11:53 +0200)]
Add mbqi interleave option, change option fs-inst to fs-interleave.
Andres Noetzli [Tue, 15 Aug 2017 05:46:48 +0000 (22:46 -0700)]
Minimize includes in expr.h: remove dups, iostream (#219)
Andres Noetzli [Tue, 15 Aug 2017 03:10:55 +0000 (20:10 -0700)]
Move function definitions from metakind.h to cpp (#218)
Andres Noetzli [Tue, 15 Aug 2017 01:34:18 +0000 (18:34 -0700)]
Move function definitions from kind.h to kind.cpp (#217)
Andres Noetzli [Mon, 14 Aug 2017 22:32:23 +0000 (15:32 -0700)]
Move function defns from smt_engine_scope.h to cpp (#216)
Additionally, this commit removes unnecessary includes, adds includes to
smt_engine.h in files that require it and removes s_smtEngine_current from
smt_engine_scope.h.
Mathias Preiner [Mon, 14 Aug 2017 18:27:53 +0000 (11:27 -0700)]
Use antlr-3.4 directory if already present in CVC4 root directory (#213)
* Find antlr-3.4 directory if installed via contrib/get-antlr-3.4.
Aina Niemetz [Mon, 14 Aug 2017 16:56:00 +0000 (09:56 -0700)]
Merge pull request #214 from CVC4/fix_warn_nonlinear
Fix compiler warnings in theory/arith/nonlinear_extension.cpp
Mark Laws [Mon, 14 Aug 2017 16:44:54 +0000 (01:44 +0900)]
Build and test suite fixes for Windows (#186)
- Build fixes for Windows
- Make proof checking tempfile handling portable
- Test suite fixes for Windows
Aina Niemetz [Sat, 12 Aug 2017 06:00:08 +0000 (23:00 -0700)]
Fix compiler warnings in theory/arith/nonlinear_extension.cpp
ajreynol [Thu, 10 Aug 2017 11:08:46 +0000 (06:08 -0500)]
Maintain frontier for tangent planes.
Andres Noetzli [Thu, 10 Aug 2017 23:55:55 +0000 (16:55 -0700)]
Fix line numbers in options_template
Mathias Preiner [Wed, 9 Aug 2017 23:44:05 +0000 (16:44 -0700)]
Fix compiler warning in src/context/context.h.
Aina Niemetz [Wed, 9 Aug 2017 23:33:23 +0000 (16:33 -0700)]
Fix help message for disable-unit-testing in configure.ac (don't -> do not)
Previous help message broke syntax highlighting in vim.
Mathias Preiner [Wed, 9 Aug 2017 22:47:27 +0000 (15:47 -0700)]
Remove AigBitblaster implementation if ABC is not compiled (#212)
* Guard use of AigBitblaster with CVC4_USE_ABC.
This removes the Unreachable() implementation of AigBitblaster in case CVC4 is
not compiled with ABC support.
Aina Niemetz [Wed, 9 Aug 2017 22:27:33 +0000 (15:27 -0700)]
Fix Assertion (compiler warning) in theory/bv/theory_bv.cpp
Andres Noetzli [Tue, 8 Aug 2017 01:16:02 +0000 (18:16 -0700)]
Fix compiler warning in sat_proof_implementation
ajreynol [Tue, 8 Aug 2017 07:40:00 +0000 (02:40 -0500)]
Use cache for datatypes cycle check, add regression.
Andrew Reynolds [Tue, 8 Aug 2017 07:05:11 +0000 (09:05 +0200)]
Merge pull request #211 from CVC4/fix_warn_sygus
Fix compiler warning in theory/quantifiers/term_database_sygus.cpp
Andres Noetzli [Tue, 8 Aug 2017 01:35:30 +0000 (18:35 -0700)]
Optionally split regression tests into test groups (#207)
To prevent timing out on Travis, this commit adds the option to split
the regression tests into groups and run each group in a separate job.
The group of a test is determined by computing a checksum of its name.
Aina Niemetz [Tue, 8 Aug 2017 00:05:47 +0000 (17:05 -0700)]
Fix compiler warning in theory/quantifiers/term_database_sygus.cpp
ajreynol [Mon, 7 Aug 2017 10:00:43 +0000 (05:00 -0500)]
Change sygus output for failed reconstruction case.
ajreynol [Mon, 7 Aug 2017 08:14:07 +0000 (03:14 -0500)]
Make quantifier elimination more robust to preprocessing.