summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-09-06Minor improvements to interface for rep set. (#2435)Andrew Reynolds
2018-09-05 More extended rewrites for strings equality (#2431)Andrew Reynolds
2018-09-05 Eliminate select over store in quantifier bodies (#2433)Andrew Reynolds
2018-09-05Use std::uniqe_ptr for d_eq_infer to make Coverity happy. (#2432)Mathias Preiner
2018-09-05Remove printing support for sygus enumeration types (#2430)Andrew Reynolds
2018-09-05Finer-grained inference of substitutions in incremental mode (#2403)Andrew Reynolds
2018-09-05Add regex grammar to rewriter verification tests (#2426)Andres Noetzli
2018-09-05 Extended rewriter for string equalities (#2427)Andrew Reynolds
2018-09-04Add HAVE_CLOCK_GETTIME guard to clock_gettime.c (#2428)Mathias Preiner
2018-09-04Remove redundant strings rewrite. (#2422)Andrew Reynolds
str.in.re( x, re.++( str.to.re(y), str.to.re(z) ) ) ---> x = str.++( y, z ) is not necessary since re.++( str.to.re(y), str.to.re(z) ) -> str.to.re( str.++( y, z ) ) str.in.re( x, str.to.re( str.++(y, z) ) ) ---> x = str.++( y, z ) This PR removes the above rewrite, which was implemented incorrectly and was dead code.
2018-09-04Update INSTALL instructions (#2420)Andres Noetzli
Fixes #2419. This commit adds more information about optional dependencies, updates macOS-related information, and fixes some details.
2018-09-04Remove CVC3 compatibility layer (#2418)Andres Noetzli
2018-09-04Remove unused options file (#2413)Andres Noetzli
2018-09-04Minor improvements to theory model builder interface. (#2408)Andrew Reynolds
2018-09-04Make quantifiers strategies exit immediately when in conflict (#2099)Andrew Reynolds
2018-09-04Transfer ownership of learned literals from SMT engine to circuit ↵Aina Niemetz
propagator. (#2421)
2018-09-04Fix merge mishap of #2359.Aina Niemetz
2018-09-04Refactor ceg conjecture initialization (#2411)Andrew Reynolds
2018-08-31Allows SAT checks of repair const to have different options (#2412)Haniel Barbosa
2018-08-31Refactor and document alpha equivalence. (#2402)Andrew Reynolds
2018-08-31Fix export of bound variables (#2409)Haniel Barbosa
2018-08-30Refactor theory preprocess into preprocessing pass. (#2395)Mathias Preiner
2018-08-30Use useBland option in FCSimplexDecisionProcedure (#2405)Andres Noetzli
2018-08-30Add regular expression elimination module (#2400)Andrew Reynolds
2018-08-29Refactor MipLibTrick preprocessing pass. (#2359)Mathias Preiner
2018-08-29Forcing attribute_internals.h to use uint64_t's for shift operations. (#2370)Tim King
2018-08-29fix bv total ops printing (#2365)Haniel Barbosa
2018-08-28 Split term canonize utility to own file and document (#2398)Andrew Reynolds
2018-08-28Reorder circuit propagator class.Aina Niemetz
2018-08-28Move flag needsFinish from SMT engine to circuit propagator.Aina Niemetz
2018-08-28 Fix for get constraints method in fmf-fun (#2399)Andrew Reynolds
2018-08-28Solve equalities between Boolean variables in presolve. (#2390)Andrew Reynolds
2018-08-28Remove throw specifiers in FP type checker (#2392)Andres Noetzli
2018-08-28Remove dead code in fp_converter (#2388)Andres Noetzli
This should fix Coverity issues 1473025 and 1459599.
2018-08-28Fix sort inference for quantified variables of interpreted types (#2393)Andrew Reynolds
2018-08-27 Address more coverity warnings (#2394)Andrew Reynolds
2018-08-27Fix warning in sygus io. (#2391)Andrew Reynolds
2018-08-27Remove dead code in evaluator (#2389)Andres Noetzli
This should fix Coverity issue 1470214.
2018-08-27Refactor extended rewriter, move rewrites to aggressive (#2387)Andrew Reynolds
This is work towards #2305. With this PR, CVC4's performance is fairly reasonable on the Kind2 BMC benchmarks with --decision=internal --ext-rew-prep --ext-rew-prep-agg.
2018-08-27New C++ API: Fix isDefinedKind() to not be ambigious with respect to … (#2384)Aina Niemetz
…underlying type.
2018-08-27Use std:unique_ptr instead of raw pointers in theory/bv. (#2385)Mathias Preiner
This should also fix CIDs 1465687, 1465695, 1465696, and 1465701.
2018-08-27Resolution proof: separate printing from proof (#1964)Andres Noetzli
Currently, we have an LFSCSatProof which inherits from TSatProof and implements printing the proof. The seperation is not clean (e.g. clauseName is used for printing only but is in TSatProof) and the inheritance does not add any value while making dependencies more confusing. The plan is that TSatProof becomes a self-contained part that the MiniSat implementations generate and ProofManager prints out. This commit is a first step in that direction. For SAT solvers with native capabilities for producing proofs, we would simply implement a different LFSC printer of their proof representation without changing the SAT solver itself. The inheritance would make this awkward to deal with. Additionally, the commit cleans up some unused functions and adjusts the visibility of TSatProof methods and members.
2018-08-27Make division chainable in the smt2 parser (#2367)Andrew Reynolds
2018-08-27Remove Coverity build from Travis (#2373)Andres Noetzli
The Coverity build is now done as part of our nightlies and the Travis Coverity build was timing out most of the time anyway, so this commit removes it.
2018-08-26Use uniform length limit for String constants (#2381)Andres Noetzli
2018-08-26Fix unsigned integer type issues in strings (#2380)Andrew Reynolds
* Fix unsigned integer types in strings. * Format
2018-08-25Refactor unconstrained simplification pass (#2374)Andres Noetzli
2018-08-25Refactor quantifier macros preprocessing pass (#1840)yoni206
Moved `src/theory/quantifiers/macros.{cpp,h}` to `src/preprocessing/passes/quantifier_macros.{cpp,h}`, and added the necessary methods for inheritance from PreprocessingPass. No need to add a test - regress0 fails when adding Assert(false) when assertions had changed.
2018-08-24Refactor nlExtPurify preprocessing pass (#1963)Haniel Barbosa
2018-08-24Clean up quantifiers engine initialization. (#2371)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback