Picky CDCL: record in the changelog

Picky CDCL: other engines instructions
usi-verification-and-security · Mar 10, 2023 · 25179f8 · 25179f8
1 parent cfc9ea9
commit 25179f8
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/Changelog.md b/Changelog.md
@@ -9,6 +9,7 @@ API changes:
 New features:
  - Implemented the interpolant production and incrementality for the Lookahead
  - Support for the combination of arrays and linear arithmetic (QF_ALIA, QF_AUFLIA)
+ - Implemented new solving heuristic - Picky CDCL, as an extension for the lookahead
 
 ### 2.4.3 (2022-11-21)
 

diff --git a/README.md b/README.md
@@ -88,6 +88,17 @@ $ opensmt test.smt2
 ```
 It is also possible to run OpenSMT without any arguments, in which case it reads the input from the standard input.
 
+### Other engines
+
+OpenSMT supports multiple SMT solving approaches. By the default it uses the approach described in the CoreSMTSolver. But it can also utilize 
+Lookahead or Picky CDCL. Those engines can be enabled by using following config:
+```
+(set-option :pure-lookahead true)
+```
+or
+```
+(set-option :picky true)
+```
 ### Interpolation
 OpenSMT supports a range of interpolation algorithms for propositional
 logic, linear real arithmetic, and uninterpreted functions with