Skip to content

Commit

Permalink
fix ToySolver.SMT to use Tseitin.Formula
Browse files Browse the repository at this point in the history
  • Loading branch information
msakai committed Oct 6, 2021
1 parent ac2e1a9 commit e400011
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/ToySolver/SMT.hs
Original file line number Diff line number Diff line change
Expand Up @@ -95,13 +95,13 @@ import Data.VectorSpace

import ToySolver.Data.Delta
import ToySolver.Data.Boolean
import ToySolver.Data.BoolExpr
import ToySolver.Data.OrdRel
import qualified ToySolver.Data.LA as LA
import qualified ToySolver.Internal.Data.Vec as Vec
import qualified ToySolver.SAT as SAT
import ToySolver.SAT.TheorySolver
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Tseitin (Formula (..))
import qualified ToySolver.Arith.Simplex as Simplex
import qualified ToySolver.BitVector as BV
import qualified ToySolver.EUF.EUFSolver as EUF
Expand Down

0 comments on commit e400011

Please sign in to comment.