summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2018-08-24 Fix more simple coverity warnings (#2372)Andrew Reynolds
2018-08-24 Remove spurious disabling of cbqi-all (#2368)Andrew Reynolds
2018-08-24Add tests that enumerate and verify rewrite rules (#2344)Andres Noetzli
2018-08-23 Do not print internally generated datatypes in external outputs with sygus ↵Andrew Reynolds
(#2234)
2018-08-23New C++ API: Add checks for kind arguments. (#2369)Aina Niemetz
This should hopefully also take care of the open coverity issues for cvc4cpp.cpp.
2018-08-23Add missing overrides in unit tests (#2362)Andres Noetzli
2018-08-23Replacing allocatedInCMM and d_noTrash with false everywhere in cdhashmap ↵Tim King
(#2355) There do not appear to be any instances these can be positive.
2018-08-23Makes the filename be set in the SMT engine by default (#2366)Haniel Barbosa
2018-08-23 Fixing some coverity warnings (#2357)Andrew Reynolds
2018-08-23Fix regression requiring proof build. (#2364)Andrew Reynolds
2018-08-23Refactor ITE simplification preprocessing pass. (#2360)Aina Niemetz
2018-08-23Use "filename" instead of "name" in SmtEngine::setInfo() (#2361)Andres Noetzli
2018-08-22global-negate preprocessing pass (#2317)yoni206
2018-08-22More regressions that increase coverage (#2354)Andrew Reynolds
2018-08-22 More unused code elimination (#2358)Andrew Reynolds
2018-08-22Generating less consistency lemmas in bv-ackermann preprocessing pass (#2253)yoni206
2018-08-22Wrapping TheorySetsPrivate in a unique_ptr. (#2356)Tim King
2018-08-22Fix option for real2int regression. (#2353)Andrew Reynolds
2018-08-22Adds regression test for automatic generation of SyGuS BV grammars (#2345)Haniel Barbosa
2018-08-22Fix invalid iterator comparisons (#2349)Andrew Reynolds
2018-08-21 Fix processing of nested Variable construct in sygus let bodies (#2351)Andrew Reynolds
2018-08-21Removing unused bool members in command.cpp. Also initializes a bool member. ↵Tim King
(#2321)
2018-08-21Warn and enable quantifiers when using sygus + logics with QF (#2352)Andrew Reynolds
2018-08-21Makes the new row propagation system default (#2335)Haniel Barbosa
2018-08-21Move d_realAssertionsEnd from SmtEnginePrivate to AssertionPipeline. (#2350)Mathias Preiner
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback