PV2 ⊧ PCSatgenerates an SMT problem from a pfwCSP spec, requires an external solver

Satisfiability checking tool for pfwCSP based on stratified Counterexample-guided Inductive Synthesis (CEGIS).

Application domain/field

• Constrained Horn Clauses (CHCs)
• Constraint-based verification
• Counterexample-guided Inductive Synthesis (CEGIS)
• Satisfiability checking
• Relational verification

Type of tool

Satisfiability checker (for pfwCSP)

Expected input

• pfwCSP problem
• Configuration file for the solver
• Solver to use

Format:

• .clp or .smt2 file which describes the pfwCSP
• .json file for configuration of the solver
• "pcsp": textual argument that is given to indicate the solver that should be used

Expected output

sat, unsat or unknown?

Internals

Uses Z3 pfwCSP: new class of predicate Constraint Satisfaction Problems. This allows constraints that are arbitrary (i.e. possibly non-Horn) clauses modulo first-order theories over predicate variables that can be functional predicates, well-founded predicates or ordinary predicates. This is a generalization over Constrained Horn Clauses.

Comments

Note: the authors sometimes call PCSat a (second-order) constraint solver