Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-08-29 | Forcing attribute_internals.h to use uint64_t's for shift operations. (#2370) | Tim King | |
2018-08-29 | fix bv total ops printing (#2365) | Haniel Barbosa | |
2018-08-28 | Split term canonize utility to own file and document (#2398) | Andrew Reynolds | |
2018-08-28 | Reorder circuit propagator class. | Aina Niemetz | |
2018-08-28 | Move 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-28 | Solve equalities between Boolean variables in presolve. (#2390) | Andrew Reynolds | |
2018-08-28 | Remove throw specifiers in FP type checker (#2392) | Andres Noetzli | |
2018-08-28 | Remove dead code in fp_converter (#2388) | Andres Noetzli | |
This should fix Coverity issues 1473025 and 1459599. | |||
2018-08-28 | Fix sort inference for quantified variables of interpreted types (#2393) | Andrew Reynolds | |
2018-08-27 | Address more coverity warnings (#2394) | Andrew Reynolds | |
2018-08-27 | Fix warning in sygus io. (#2391) | Andrew Reynolds | |
2018-08-27 | Remove dead code in evaluator (#2389) | Andres Noetzli | |
This should fix Coverity issue 1470214. | |||
2018-08-27 | Refactor 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-27 | New C++ API: Fix isDefinedKind() to not be ambigious with respect to … (#2384) | Aina Niemetz | |
…underlying type. | |||
2018-08-27 | Use 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-27 | Resolution 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-27 | Make division chainable in the smt2 parser (#2367) | Andrew Reynolds | |
2018-08-27 | Remove 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-26 | Use uniform length limit for String constants (#2381) | Andres Noetzli | |
2018-08-26 | Fix unsigned integer type issues in strings (#2380) | Andrew Reynolds | |
* Fix unsigned integer types in strings. * Format | |||
2018-08-25 | Refactor unconstrained simplification pass (#2374) | Andres Noetzli | |
2018-08-25 | Refactor 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-24 | Refactor nlExtPurify preprocessing pass (#1963) | Haniel Barbosa | |
2018-08-24 | Clean 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-24 | Add 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-23 | New 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-23 | Add missing overrides in unit tests (#2362) | Andres Noetzli | |
2018-08-23 | Replacing 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-23 | Makes 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-23 | Fix regression requiring proof build. (#2364) | Andrew Reynolds | |
2018-08-23 | Refactor ITE simplification preprocessing pass. (#2360) | Aina Niemetz | |
2018-08-23 | Use "filename" instead of "name" in SmtEngine::setInfo() (#2361) | Andres Noetzli | |
2018-08-22 | global-negate preprocessing pass (#2317) | yoni206 | |
2018-08-22 | More regressions that increase coverage (#2354) | Andrew Reynolds | |
2018-08-22 | More unused code elimination (#2358) | Andrew Reynolds | |
2018-08-22 | Generating less consistency lemmas in bv-ackermann preprocessing pass (#2253) | yoni206 | |
2018-08-22 | Wrapping TheorySetsPrivate in a unique_ptr. (#2356) | Tim King | |
2018-08-22 | Fix option for real2int regression. (#2353) | Andrew Reynolds | |
2018-08-22 | Adds regression test for automatic generation of SyGuS BV grammars (#2345) | Haniel Barbosa | |
2018-08-22 | Fix invalid iterator comparisons (#2349) | Andrew Reynolds | |
2018-08-21 | Fix processing of nested Variable construct in sygus let bodies (#2351) | Andrew Reynolds | |
2018-08-21 | Removing unused bool members in command.cpp. Also initializes a bool member. ↵ | Tim King | |
(#2321) | |||
2018-08-21 | Warn and enable quantifiers when using sygus + logics with QF (#2352) | Andrew Reynolds | |
2018-08-21 | Makes the new row propagation system default (#2335) | Haniel Barbosa | |
2018-08-21 | Move d_realAssertionsEnd from SmtEnginePrivate to AssertionPipeline. (#2350) | Mathias Preiner | |